set X = { x where x is POINT of S : Collinear p,q,x } ;
{ x where x is POINT of S : Collinear p,q,x } c= the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is POINT of S : Collinear p,q,x } or x in the carrier of S )
assume x in { x where x is POINT of S : Collinear p,q,x } ; :: thesis: x in the carrier of S
then ex y being POINT of S st
( x = y & Collinear p,q,y ) ;
hence x in the carrier of S ; :: thesis: verum

end;

hence { x where x is POINT of S : Collinear p,q,x } is Subset of S ; :: thesis: verum