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$.

Parents

Subset of

Bipartite graph