Bipartite complete graph

Set

 context $V,E$ … set
 definiendum $\langle V,E,\psi\rangle \in \mathrm{it}(E,V)$
 postulate $\langle V,E,\psi\rangle$ … undirected graph
 range $X\cap Y=\emptyset$ range $x\in X$ range $y\in Y$
 postulate $\exists X,Y.\ (\forall u,v.\ \{u,v\}\in\mathrm{im}(\psi)\implies (u\in X\land v\in Y)\lor (v\in X\land u\in Y)) \land (\forall x,y.\ \{x,y\}\in\mathrm{im}\ \psi)$

Discussion

Let $G$ be a bipartite complete graph with parts $X$ and $Y$. Then $G$ is bipartite complete if each $x\in X$ connects to each $y\in Y$.