let P be Subset of (TOP-REAL 2); for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
let p1, p2 be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 implies ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) )
assume A1:
P is_an_arc_of p1,p2
; ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
A2:
now ( p1 = y_Middle (P,p1,p2) implies p1 `2 = p2 `2 )assume A3:
p1 = y_Middle (
P,
p1,
p2)
;
p1 `2 = p2 `2 deffunc H1(
Point of
(TOP-REAL 2))
-> Point of
(TOP-REAL 2) = $1;
defpred S1[
Point of
(TOP-REAL 2)]
means $1
`2 = ((p1 `2) + (p2 `2)) / 2;
reconsider Q1 =
{ H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as
Subset of
(TOP-REAL 2) from DOMAIN_1:sch 8();
A4:
P meets Q1
by A1, Th14;
A5:
P /\ Q1 is
closed
by A1, Th14;
y_Middle (
P,
p1,
p2)
= First_Point (
P,
p1,
p2,
Q1)
by Def2;
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 `2 = ((p1 `2) + (p2 `2)) / 2 )
;
hence
p1 `2 = p2 `2
;
verum end;
now ( p1 `2 = p2 `2 implies p1 = y_Middle (P,p1,p2) )assume A6:
p1 `2 = p2 `2
;
p1 = y_Middle (P,p1,p2)
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
p1 = First_Point (
P,
p1,
p2,
Q)
proof
let Q be
Subset of
(TOP-REAL 2);
( Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies p1 = First_Point (P,p1,p2,Q) )
assume A7:
Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 }
;
p1 = First_Point (P,p1,p2,Q)
then A8:
p1 in Q
by A6;
P /\ Q is
closed
by A1, A7, Th14;
hence
p1 = First_Point (
P,
p1,
p2,
Q)
by A1, A8, JORDAN5C:3;
verum
end; hence
p1 = y_Middle (
P,
p1,
p2)
by Def2;
verum end;
hence
( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
by A2; verum