let G be set ; :: thesis: ( G is void implies PairsOf G = {} )
assume A: G is void ; :: thesis: PairsOf G = {}
assume PairsOf G <> {} ; :: thesis: contradiction
then consider x being set such that
B: x in PairsOf G by XBOOLE_0:def 1;
D: card x = 2 by B, LEdges;
G = {{}} by A, Lvoid;
then x = {} by B, TARSKI:def 1;
hence contradiction by D; :: thesis: verum