set TL = { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } c= (Terminals G) *

proof

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

end;

hence { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *) ; :: thesis: verum