set M = { n where n is positive Nat : n '*' (1. R) = 0. R } ;

now :: thesis: for x being object st x in { n where n is positive Nat : n '*' (1. R) = 0. R } holds
x in NAT

let x be object ; :: thesis: ( x in { n where n is positive Nat : n '*' (1. R) = 0. R } implies x in NAT )
assume x in { n where n is positive Nat : n '*' (1. R) = 0. R } ; :: thesis: x in NAT
then consider k being positive Nat such that
A1: ( x = k & k '*' (1. R) = 0. R ) ;
thus x in NAT by A1, ORDINAL1:def 12; :: thesis: verum

end;

then { n where n is positive Nat : n '*' (1. R) = 0. R } c= NAT ;
hence { n where n is positive Nat : n '*' (1. R) = 0. R } is Subset of NAT ; :: thesis: verum