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

now :: thesis: for x being object st x in { z where z is POINT of IPS : z on Z } holds

x in the Points of IPS

hence
{ z where z is POINT of IPS : z on Z } is Subset of the Points of IPS
by TARSKI:def 3; :: thesis: verumx in the Points of IPS

let x be object ; :: 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;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