let G, x be set ; :: thesis: ( card (union G) = 1 implies G is pairfree )
assume A: card (union G) = 1 ; :: thesis: G is pairfree
assume not G is pairfree ; :: thesis: contradiction
then PairsOf G <> {} by Ledgeless;
then consider e being set such that
C: e in PairsOf G by XBOOLE_0:def 1;
consider x, y being set such that
D: x <> y and
E: x in union G and
F: y in union G and
e = {x,y} by C, SG4;
consider w being set such that
H: union G = {w} by A, CARD_2:42;
x = w by E, H, TARSKI:def 1;
hence contradiction by D, F, H, TARSKI:def 1; :: thesis: verum