let n be Nat; :: thesis: not n is pair

given x, y being object such that A1: n = [x,y] ; :: according to XTUPLE_0:def 1 :: thesis: contradiction

n <> 0 by A1;

then 0 < n ;

then 0 in Segm n by NAT_1:44;

hence contradiction by A1, TARSKI:def 2; :: thesis: verum

given x, y being object such that A1: n = [x,y] ; :: according to XTUPLE_0:def 1 :: thesis: contradiction

n <> 0 by A1;

then 0 < n ;

then 0 in Segm n by NAT_1:44;

hence contradiction by A1, TARSKI:def 2; :: thesis: verum