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 )
reconsider m = n as Element of NAT by ORDINAL1:def 12;
assume x in n ; :: thesis: x is Nat
then x in { j where j is Element of NAT : j < m } by AXIOMS:4;
then ex j being Element of NAT st
( x = j & j < m ) ;
hence x is Nat ; :: thesis: verum