let G be set ; :: thesis: for x, y being object st {x,y} in PairsOf G holds
( x <> y & x in union G & y in union G )
let a, b be object ; :: 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
A1: x <> y and
A2: ( x in union G & y in union G ) and
A3: {a,b} = {x,y} by Th11;
( ( a = x & b = y ) or ( a = y & b = x ) ) by A3, ZFMISC_1:6;
hence ( a <> b & a in union G & b in union G ) by A2, A1; :: thesis: verum