let x be pair set ; :: according to FACIRC_1:def 2 :: thesis: not x in NAT
assume x in NAT ; :: thesis: contradiction
hence contradiction ; :: thesis: verum