let q3, q4 be Point of (TOP-REAL 2); :: thesis: ( ( 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

q3 = First_Point (P,p1,p2,Q) ) & ( 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

q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 )

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

q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of (TOP-REAL 2) st Q2 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `2 = ((p1 `2) + (p2 `2)) / 2 } holds

q4 = First_Point (P,p1,p2,Q2) ) ) ; :: thesis: q3 = q4

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

q3 = First_Point (P,p1,p2,Q3) by A1;

hence q3 = q4 by A1; :: thesis: verum

q3 = First_Point (P,p1,p2,Q) ) & ( 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

q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 )

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

q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of (TOP-REAL 2) st Q2 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `2 = ((p1 `2) + (p2 `2)) / 2 } holds

q4 = First_Point (P,p1,p2,Q2) ) ) ; :: thesis: q3 = q4

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

proof

then reconsider Q3 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `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 { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } or x in the carrier of (TOP-REAL 2) )

assume x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `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 { q1 where q1 is Point of (TOP-REAL 2) : q1 `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

q3 = First_Point (P,p1,p2,Q3) by A1;

hence q3 = q4 by A1; :: thesis: verum