let G, a, b be set ; :: thesis: ( {a,b} in PairsOf G implies ( a <> b & a in union G & b in union G ) )
assume {a,b} in PairsOf G ; :: thesis: ( a <> b & a in union G & b in union G )
then consider x, y being set such that
C: x <> y and
A: ( x in union G & y in union G ) and
B: {a,b} = {x,y} by SG4;
( ( a = x & b = y ) or ( a = y & b = x ) ) by B, ZFMISC_1:6;
hence ( a <> b & a in union G & b in union G ) by A, C; :: thesis: verum