let a be non empty set ; :: thesis: ex b being object st
for x being set holds not [x,b] in a
reconsider b = { u where u is Element of a : ex y, z being set st
( [y,z] = u & not u in z ) } as set ;
A1: for x being set st [x,b] in b holds
( [x,b] in a & not [x,b] in b )

proof

let x be set ; :: thesis: ( [x,b] in b implies ( [x,b] in a & not [x,b] in b ) )
assume [x,b] in b ; :: thesis: ( [x,b] in a & not [x,b] in b )
then consider u1 being Element of a such that
A3: ( u1 = [x,b] & ex y, z being set st
( [y,z] = u1 & not u1 in z ) ) ;
thus ( [x,b] in a & not [x,b] in b ) by A3, XTUPLE_0:1; :: thesis: verum

end;

A4: for x being set holds not [x,b] in a

proof

let x be set ; :: thesis: not [x,b] in a
assume A5: [x,b] in a ; :: thesis: contradiction

per cases ( [x,b] in b or not [x,b] in b ) ;

suppose [x,b] in b ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose not [x,b] in b ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

end;

end;

take b ; :: thesis: for x being set holds not [x,b] in a
thus for x being set holds not [x,b] in a by A4; :: thesis: verum