let x be set ; :: thesis: for n being Nat st x in n holds
x is Nat
let n be Nat; :: thesis: ( x in n implies x is Nat )
assume A1: x in n ; :: thesis: x is Nat
reconsider m = n as Element of NAT by ORDINAL1:def 13;
x in { j where j is Element of NAT : j < m } by A1, AXIOMS:30;
then ex j being Element of NAT st
( x = j & j < m ) ;
hence x is Nat ; :: thesis: verum