set IT = { (ord a) where a is Element of G : verum } ;

{ (ord a) where a is Element of G : verum } c= NAT

{ (ord a) where a is Element of G : verum } c= NAT

proof

hence
{ (ord a) where a is Element of G : verum } is Subset of NAT
; :: thesis: verum
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;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