let G be set ; :: thesis: ( G is void implies PairsOf G = {} )
assume A1: G is void ; :: thesis: PairsOf G = {}
assume PairsOf G <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in PairsOf G by XBOOLE_0:def 1;
reconsider x = x as set by TARSKI:1;
A3: card x = 2 by A2, Def1;
G = {{}} by A1;
then x = {} by A2, TARSKI:def 1;
hence contradiction by A3; :: thesis: verum