{ x where x is POINT of S : A out x,a } 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 : A out x,a } or x in the carrier of S )
assume x in { x where x is POINT of S : A out x,a } ; :: thesis: x in the carrier of S
then ex y being POINT of S st
( x = y & A out y,a ) ;
hence x in the carrier of S ; :: thesis: verum

end;

hence { x where x is POINT of S : A out x,a } is Subset of S ; :: thesis: verum