{ q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } c= the carrier of (TOP-REAL 2)

reconsider q2 = First_Point (P,p1,p2,Q1) as Point of (TOP-REAL 2) ;

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

q2 = First_Point (P,p1,p2,Q) ;

hence ex b_{1} being Point of (TOP-REAL 2) st

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b_{1} = First_Point (P,p1,p2,Q)
; :: thesis: verum

proof

then reconsider Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } as Subset of (TOP-REAL 2) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } or x in the carrier of (TOP-REAL 2) )

assume x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; :: thesis: x in the carrier of (TOP-REAL 2)

then ex q being Point of (TOP-REAL 2) st

( q = x & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ;

hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; :: thesis: x in the carrier of (TOP-REAL 2)

then ex q being Point of (TOP-REAL 2) st

( q = x & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ;

hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

reconsider q2 = First_Point (P,p1,p2,Q1) as Point of (TOP-REAL 2) ;

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

q2 = First_Point (P,p1,p2,Q) ;

hence ex b

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b