let G, x be set ; :: thesis: ( card (union G) = 1 implies G is pairfree )
assume A1: card (union G) = 1 ; :: thesis: G is pairfree
assume not G is pairfree ; :: thesis: contradiction
then PairsOf G <> {} ;
then consider e being object such that
A2: e in PairsOf G by XBOOLE_0:def 1;
consider x, y being set such that
A3: x <> y and
A4: x in union G and
A5: y in union G and
e = {x,y} by A2, Th11;
consider w being object such that
A6: union G = {w} by A1, CARD_2:42;
x = w by A4, A6, TARSKI:def 1;
hence contradiction by A3, A5, A6, TARSKI:def 1; :: thesis: verum