{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } c= the carrier of (TOP-REAL 2)
proof
let x be
object ;
TARSKI:def 3 ( not x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } or x in the carrier of (TOP-REAL 2) )
assume
x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 }
;
x in the carrier of (TOP-REAL 2)
then
ex
q being
Point of
(TOP-REAL 2) st
(
q = x &
LE q,
q1,
P,
p1,
p2 )
;
hence
x in the
carrier of
(TOP-REAL 2)
;
verum
end;
hence
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2)
; verum