now :: thesis: for x being object st x in { (t * a) where a is Point of T : a in A } holds
x in the carrier of T

let x be object ; :: thesis: ( x in { (t * a) where a is Point of T : a in A } implies x in the carrier of T )
assume x in { (t * a) where a is Point of T : a in A } ; :: thesis: x in the carrier of T
then ex q being Point of T st
( x = t * q & q in A ) ;
hence x in the carrier of T ; :: thesis: verum

end;

hence { (t * a) where a is Point of T : a in A } is Subset of T by TARSKI:def 3; :: thesis: verum