let q3, q4 be Point of (); :: thesis: ( ( for Q being Subset of () st Q = { q where q is Point of () : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q3 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of () st Q = { q where q is Point of () : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 )

assume A1: ( ( for Q1 being Subset of () st Q1 = { q1 where q1 is Point of () : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of () st Q2 = { q2 where q2 is Point of () : q2 `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q4 = First_Point (P,p1,p2,Q2) ) ) ; :: thesis: q3 = q4
{ q1 where q1 is Point of () : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q1 where q1 is Point of () : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } or x in the carrier of () )
assume x in { q1 where q1 is Point of () : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } ; :: thesis: x in the carrier of ()
then ex q being Point of () st
( q = x & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ;
hence x in the carrier of () ; :: thesis: verum
end;
then reconsider Q3 = { q2 where q2 is Point of () : q2 `1 = ((p1 `1) + (p2 `1)) / 2 } as Subset of () ;
q3 = First_Point (P,p1,p2,Q3) by A1;
hence q3 = q4 by A1; :: thesis: verum