let n be Nat; :: thesis: not n is pair
given x, y being set such that A1: n = [x,y] ; :: according to FACIRC_1:def 1 :: thesis: contradiction
n = { k where k is Element of NAT : k < n } by AXIOMS:4;
then 0 in n by A1;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum