theorem Th3: :: FIELD_3:2

for n being Nat
for x, y being object st n = {x,y} & x <> y & not ( x = 0 & y = 1 ) holds
( x = 1 & y = 0 )