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 object such that
A2: ( x in A & y in A & not x = y ) and
A3: {e1,e2} = {x,y} by Th8;
per cases ( ( e1 = x & e2 = x ) or ( e1 = x & e2 = y ) or ( e1 = y & e2 = x ) or ( e1 = y & e2 = y ) ) by A3, ZFMISC_1:6;
suppose ( e1 = x & e2 = x ) ; :: thesis: ( e1 in A & e2 in A & e1 <> e2 )
then {x} in TWOELEMENTSETS A by A1, ENUMSET1:29;
then ex x1, x2 being object st
( x1 in A & x2 in A & not x1 = x2 & {x} = {x1,x2} ) by Th8;
hence ( e1 in A & e2 in A & e1 <> e2 ) by ZFMISC_1:5; :: 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:29;
then ex x1, x2 being object st
( x1 in A & x2 in A & not x1 = x2 & {y} = {x1,x2} ) by Th8;
hence ( e1 in A & e2 in A & e1 <> e2 ) by ZFMISC_1:5; :: thesis: verum
end;
end;