set X = { z where z is POINT of IPS : z on Z } ;
{ z where z is POINT of IPS : z on Z } c= the Points of IPS

proof

now

let x be set ; :: thesis: ( x in { z where z is POINT of IPS : z on Z } implies x in the Points of IPS )
assume x in { z where z is POINT of IPS : z on Z } ; :: thesis: x in the Points of IPS
then ex z being POINT of IPS st
( z = x & z on Z ) ;
hence x in the Points of IPS ; :: thesis: verum

end;

hence { z where z is POINT of IPS : z on Z } c= the Points of IPS by TARSKI:def 3; :: thesis: verum

end;

hence { z where z is POINT of IPS : z on Z } is Subset of the Points of IPS ; :: thesis: verum