let x be set ; :: thesis: for i being Nat st x in i holds
x is Element of NAT
let i be Nat; :: thesis: ( x in i implies x is Element of NAT )
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
A1: i0 c= NAT by MEMBERED:6;
assume x in i ; :: thesis: x is Element of NAT
hence x is Element of NAT by A1; :: thesis: verum