let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in NAT or [x,x] in NATOrd )
assume x in NAT ; :: thesis: [x,x] in NATOrd
then reconsider x9 = x as Element of NAT ;
x9 <= x9 ;
hence [x,x] in NATOrd ; :: thesis: verum