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