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 )
A2:
now assume A3:
p1 = x_Middle P,
p1,
p2
;
:: thesis: p1 `1 = p2 `1 deffunc H1(
Point of
(TOP-REAL 2))
-> Point of
(TOP-REAL 2) = $1;
defpred S1[
Point of
(TOP-REAL 2)]
means $1
`1 = ((p1 `1 ) + (p2 `1 )) / 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 &
P /\ Q1 is
closed )
by A1, Th14;
x_Middle P,
p1,
p2 = First_Point P,
p1,
p2,
Q1
by Def1;
then
p1 in P /\ Q1
by A1, A3, A4, 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;
now assume A5:
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
proof
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 A6:
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 A7:
p1 in Q
by A5;
(
P meets Q &
P /\ Q is
closed )
by A1, A6, Th14;
hence
p1 = First_Point P,
p1,
p2,
Q
by A1, A7, JORDAN5C:3;
:: thesis: verum
end; hence
p1 = x_Middle P,
p1,
p2
by Def1;
:: thesis: verum end;
hence
( p1 = x_Middle P,p1,p2 iff p1 `1 = p2 `1 )
by A2; :: thesis: verum