set TL = { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
{ (PostTraversal 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (PostTraversal 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 { (PostTraversal 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 consider tsg being Element of FinTrees the carrier of G such that
A3: ( x = PostTraversal tsg & tsg in TS G & tsg . {} = nt ) ;
thus x in the carrier of G * by A3, FINSEQ_1:def 11; :: thesis: verum

end;

hence { (PostTraversal 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