let n be Nat; :: thesis: n is natural-membered

now :: thesis: for x being object st x in n holds
x is natural

let x be object ; :: thesis: ( x in n implies x is natural )
assume A1: x in n ; :: thesis: x is natural
n in omega by ORDINAL1:def 12;
then x in omega by A1, ORDINAL1:10;
hence x is natural ; :: thesis: verum

end;

hence n is natural-membered by MEMBERED:def 6; :: thesis: verum