let n be Nat; :: thesis: for x, y being object st n = {x,y} & x <> y & not ( x = 0 & y = 1 ) holds
( x = 1 & y = 0 )
let x, y be object ; :: thesis: ( n = {x,y} & x <> y & not ( x = 0 & y = 1 ) implies ( x = 1 & y = 0 ) )
assume A1: ( n = {x,y} & x <> y ) ; :: thesis: ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) )
then card n = 2 by CARD_2:57;
then A2: ( x in {0,1} & y in {0,1} ) by A1, CARD_1:50, TARSKI:def 2;
per cases ( x = 0 or x = 1 ) by A2, TARSKI:def 2;
suppose x = 0 ; :: thesis: ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) )
hence ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) ) by A1, A2, TARSKI:def 2; :: thesis: verum
end;
suppose x = 1 ; :: thesis: ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) )
hence ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) ) by A1, A2, TARSKI:def 2; :: thesis: verum
end;
end;