{ t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } c= Union the Sorts of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } or a in Union the Sorts of T )
assume a in { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ; :: thesis: a in Union the Sorts of T
then ex t being Element of (Free (S,X)) st
( a = t & t in T & height t <= i ) ;
hence a in Union the Sorts of T ; :: thesis: verum

end;

hence { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } is Subset of T ; :: thesis: verum