set IT = { (ord a) where a is Element of G : verum } ;
{ (ord a) where a is Element of G : verum } c= NAT
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (ord a) where a is Element of G : verum } or a in NAT )
assume a in { (ord a) where a is Element of G : verum } ; :: thesis: a in NAT
then consider n being Element of G such that
A1: a = ord n ;
thus a in NAT by A1; :: thesis: verum
end;
hence { (ord a) where a is Element of G : verum } is Subset of NAT ; :: thesis: verum