set TL = { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
{ (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } c= the carrier of G *
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in the carrier of G * )
assume x in { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; :: thesis: x in the carrier of G *
then ex tsg being Element of FinTrees the carrier of G st
( x = PreTraversal tsg & tsg in TS G & tsg . {} = nt ) ;
hence x in the carrier of G * by FINSEQ_1:def 11; :: thesis: verum
end;
hence { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *) ; :: thesis: verum