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)

proof

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

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) ;
q3 = First_Point (P,p1,p2,Q3) by A1;
hence q3 = q4 by A1; :: thesis: verum