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