A finite graph is bipartite if and only if it has no odd cycle

Suppose $G$ has a bipartition $(A,B)$. Along any walk the successive vertices alternate between $A$ and $B$, so a closed walk returns to its initial part only after an even number of edges. In particular, every cycle has even length.

Conversely, suppose $G$ has no odd cycle. Then by [L1] it has no odd closed walk.

Let $C$ be an arbitrary connected component. It is nonempty by [L2], so fix a root $r\in C$. Put $A_C$ equal to the vertices joined to $r$ by an even-length path and $B_C$ equal to those joined to $r$ by an odd-length path. Every vertex of $C$ lies in at least one of these sets by [F2]. This construction is vacuous when the graph has no components.

The sets $A_C$ and $B_C$ are disjoint: an even $r$ to $v$ path followed by the reverse of an odd $r$ to $v$ path would be an odd closed walk, contrary to step 1.2.

Every edge $\{u,v\}$ inside $C$ runs between $A_C$ and $B_C$. Otherwise choose paths from $r$ to $u$ and from $r$ to $v$ having the common parity of their class. Traversing the first path, the edge $\{u,v\}$, and the reverse of the second path gives an odd closed walk, contrary to step 1.2.

By [L2], the connected components partition the finite vertex set and therefore form a finite family. Repeating this construction for each component and taking $A$ and $B$ to be the unions of their respective parts gives disjoint sets with $V=A\cup B$. The endpoints of an edge are joined by that one-edge path and hence lie in one component by [F2], so every edge runs between the two global parts. Thus $(A,B)$ is a bipartition.

Step 1.1 proves that bipartite graphs have no odd cycle, and steps 1.2 to 5.1 prove the converse.