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 `1 = ((p1 `1 ) + (p2 `1 )) / 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 `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
q4 = First_Point P,p1,p2,Q ) implies q3 = q4 )
assume A2: ( ( for Q1 being Subset of (TOP-REAL 2) st Q1 = { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1 ) + (p2 `1 )) / 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 `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
q4 = First_Point P,p1,p2,Q2 ) ) ; :: thesis: q3 = q4
{ q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1 ) + (p2 `1 )) / 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 `1 = ((p1 `1 ) + (p2 `1 )) / 2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1 ) + (p2 `1 )) / 2 } ; :: thesis: x in the carrier of (TOP-REAL 2)
then consider q being Point of (TOP-REAL 2) such that
A3: ( q = x & q `1 = ((p1 `1 ) + (p2 `1 )) / 2 ) ;
thus x in the carrier of (TOP-REAL 2) by A3; :: thesis: verum

end;

then reconsider Q3 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `1 = ((p1 `1 ) + (p2 `1 )) / 2 } as Subset of (TOP-REAL 2) ;
q3 = First_Point P,p1,p2,Q3 by A2;
hence q3 = q4 by A2; :: thesis: verum