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