let A be set ; :: thesis: for e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A & e2 in A & e1 <> e2 )
let e1, e2 be set ; :: thesis: ( {e1,e2} in TWOELEMENTSETS A implies ( e1 in A & e2 in A & e1 <> e2 ) )
assume A1: {e1,e2} in TWOELEMENTSETS A ; :: thesis: ( e1 in A & e2 in A & e1 <> e2 )
then consider x, y being set such that
A2: ( x in A & y in A & not x = y & {e1,e2} = {x,y} ) by Th10;

per cases ( ( e1 = x & e2 = x ) or ( e1 = x & e2 = y ) or ( e1 = y & e2 = x ) or ( e1 = y & e2 = y ) ) by A2, ZFMISC_1:10;

suppose ( e1 = x & e2 = x ) ; :: thesis: ( e1 in A & e2 in A & e1 <> e2 )

then {x} in TWOELEMENTSETS A by A1, ENUMSET1:69;
then consider x1, x2 being set such that
A3: ( x1 in A & x2 in A & not x1 = x2 & {x} = {x1,x2} ) by Th10;
thus ( e1 in A & e2 in A & e1 <> e2 ) by A3, ZFMISC_1:9; :: thesis: verum

end;

suppose ( e1 = x & e2 = y ) ; :: thesis: ( e1 in A & e2 in A & e1 <> e2 )

hence ( e1 in A & e2 in A & e1 <> e2 ) by A2; :: thesis: verum

end;

suppose ( e1 = y & e2 = x ) ; :: thesis: ( e1 in A & e2 in A & e1 <> e2 )

hence ( e1 in A & e2 in A & e1 <> e2 ) by A2; :: thesis: verum

end;

suppose ( e1 = y & e2 = y ) ; :: thesis: ( e1 in A & e2 in A & e1 <> e2 )

then {y} in TWOELEMENTSETS A by A1, ENUMSET1:69;
then consider x1, x2 being set such that
A4: ( x1 in A & x2 in A & not x1 = x2 & {y} = {x1,x2} ) by Th10;
thus ( e1 in A & e2 in A & e1 <> e2 ) by A4, ZFMISC_1:9; :: thesis: verum

end;

end;