now :: thesis: for x being object st x in { y where y is Point of T : B + y c= X } holds
x in the carrier of T

let x be object ; :: thesis: ( x in { y where y is Point of T : B + y c= X } implies x in the carrier of T )
assume x in { y where y is Point of T : B + y c= X } ; :: thesis: x in the carrier of T
then ex q being Point of T st
( x = q & B + q c= X ) ;
hence x in the carrier of T ; :: thesis: verum

end;

hence { y where y is Point of T : B + y c= X } is Subset of T by TARSKI:def 3; :: thesis: verum