\documentclass{article}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}

\theoremstyle{definition}
\newtheorem{definition}{Definition}

\theoremstyle{theorem}
\newtheorem{theorem}{Theorem}

\title{Main Theorem Extraction: Partitioning the Plane}
\date{}

\begin{document}

\maketitle

\section*{Definitions}

\begin{definition}[Rectangle of Area 1]
A set $s \subset \mathbb{C}$ is said to form a \textit{rectangle of area 1} if there exist distinct points $z_1, z_2, z_3, z_4$ such that $s = \{z_1, z_2, z_3, z_4\}$ and the following conditions hold:
\begin{enumerate}
    \item $z_2 - z_1 = z_3 - z_4$ (The points form a parallelogram),
    \item $\mathrm{Re}((z_2 - z_1) \cdot \overline{(z_4 - z_1)}) = 0$ (The adjacent sides are perpendicular),
    \item $|z_2 - z_1|^2 \cdot |z_4 - z_1|^2 = 1$ (The square of the area is 1).
\end{enumerate}
\end{definition}

\section*{Main Theorem}

\begin{theorem}
It is possible to partition $\mathbb{C}$ (identified with $\mathbb{R}^2$) into 25 color classes such that none of them contains the vertices of a rectangle of area 1.

Formally, there exists a function $f : \mathbb{C} \to \{0, \dots, 24\}$ such that for every color $c \in \{0, \dots, 24\}$, there does not exist a set $s \subset \mathbb{C}$ satisfying:
\[ s \subseteq f^{-1}(\{c\}) \land \text{IsRectangleArea1}(s) \]
\end{theorem}

\end{document}