let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

A2: now :: thesis: ( p1 = x_Middle (P,p1,p2) implies p1 `1 = p2 `1 )

assume A3:
p1 = x_Middle (P,p1,p2)
; :: thesis: p1 `1 = p2 `1

deffunc H_{1}( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1;

defpred S_{1}[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1) + (p2 `1)) / 2;

reconsider Q1 = { H_{1}(q) where q is Point of (TOP-REAL 2) : S_{1}[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 8();

A4: P meets Q1 by A1, Th13;

A5: P /\ Q1 is closed by A1, Th13;

x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def1;

then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def 1;

then p1 in Q1 by XBOOLE_0:def 4;

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

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

hence p1 `1 = p2 `1 ; :: thesis: verum

end;deffunc H

defpred S

reconsider Q1 = { H

A4: P meets Q1 by A1, Th13;

A5: P /\ Q1 is closed by A1, Th13;

x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def1;

then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def 1;

then p1 in Q1 by XBOOLE_0:def 4;

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

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

hence p1 `1 = p2 `1 ; :: thesis: verum

now :: thesis: ( p1 `1 = p2 `1 implies p1 = x_Middle (P,p1,p2) )

hence
( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )
by A2; :: thesis: verumassume A6:
p1 `1 = p2 `1
; :: thesis: p1 = x_Middle (P,p1,p2)

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

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

end;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

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

proof

hence
p1 = x_Middle (P,p1,p2)
by Def1; :: thesis: verum
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies p1 = First_Point (P,p1,p2,Q) )

assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; :: thesis: p1 = First_Point (P,p1,p2,Q)

then A8: p1 in Q by A6;

P /\ Q is closed by A1, A7, Th13;

hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; :: thesis: verum

end;assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; :: thesis: p1 = First_Point (P,p1,p2,Q)

then A8: p1 in Q by A6;

P /\ Q is closed by A1, A7, Th13;

hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; :: thesis: verum