let P be non empty Subset of (TOP-REAL 2); for p1, p2, q1, q2, p being Point of (TOP-REAL 2)
for e being Real st q1 is_Rout P,p1,p2,e & q2 `1 = e & LSeg (q1,q2) c= P & p in LSeg (q1,q2) holds
p is_Rout P,p1,p2,e
let p1, p2, q1, q2, p be Point of (TOP-REAL 2); for e being Real st q1 is_Rout P,p1,p2,e & q2 `1 = e & LSeg (q1,q2) c= P & p in LSeg (q1,q2) holds
p is_Rout P,p1,p2,e
let e be Real; ( q1 is_Rout P,p1,p2,e & q2 `1 = e & LSeg (q1,q2) c= P & p in LSeg (q1,q2) implies p is_Rout P,p1,p2,e )
assume that
A1:
q1 is_Rout P,p1,p2,e
and
A2:
q2 `1 = e
and
A3:
LSeg (q1,q2) c= P
and
A4:
p in LSeg (q1,q2)
; p is_Rout P,p1,p2,e
A5:
q1 in P
by A1;
A6:
q2 in LSeg (q1,q2)
by RLTOPSP1:68;
A7:
q1 `1 = e
by A1;
consider p4 being Point of (TOP-REAL 2) such that
A8:
p4 `1 > e
and
A9:
LE q1,p4,P,p1,p2
and
A10:
for p5 being Point of (TOP-REAL 2) st LE p5,p4,P,p1,p2 & LE q1,p5,P,p1,p2 holds
p5 `1 >= e
by A1;
A11:
P is_an_arc_of p1,p2
by A1;
A12:
p4 in P
by A9, JORDAN5C:def 3;
now ( ( LE q2,q1,P,p1,p2 & p is_Rout P,p1,p2,e ) or ( LE q1,q2,P,p1,p2 & p is_Rout P,p1,p2,e ) )per cases
( LE q2,q1,P,p1,p2 or LE q1,q2,P,p1,p2 )
by A3, A11, A5, A6, Th19;
case A13:
LE q2,
q1,
P,
p1,
p2
;
p is_Rout P,p1,p2,eA14:
now ( ( q1 <> q2 & Segment (P,p1,p2,q2,q1) = LSeg (q2,q1) ) or ( q1 = q2 & Segment (P,p1,p2,q2,q1) = LSeg (q2,q1) ) )per cases
( q1 <> q2 or q1 = q2 )
;
case
q1 <> q2
;
Segment (P,p1,p2,q2,q1) = LSeg (q2,q1)then
LSeg (
q2,
q1)
is_an_arc_of q2,
q1
by TOPREAL1:9;
hence
Segment (
P,
p1,
p2,
q2,
q1)
= LSeg (
q2,
q1)
by A3, A11, A13, Th25;
verum end; end; end;
Segment (
P,
p1,
p2,
q2,
q1)
= { p3 where p3 is Point of (TOP-REAL 2) : ( LE q2,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) }
by JORDAN6:26;
then A16:
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 &
LE q2,
p3,
P,
p1,
p2 &
LE p3,
q1,
P,
p1,
p2 )
by A4, A14;
then A17:
LE p,
p4,
P,
p1,
p2
by A9, JORDAN5C:13;
A18:
for
p6 being
Point of
(TOP-REAL 2) st
LE p6,
p4,
P,
p1,
p2 &
LE p,
p6,
P,
p1,
p2 holds
p6 `1 >= e
proof
let p6 be
Point of
(TOP-REAL 2);
( LE p6,p4,P,p1,p2 & LE p,p6,P,p1,p2 implies p6 `1 >= e )
assume that A19:
LE p6,
p4,
P,
p1,
p2
and A20:
LE p,
p6,
P,
p1,
p2
;
p6 `1 >= e
A21:
p6 in P
by A19, JORDAN5C:def 3;
now ( ( LE q1,p6,P,p1,p2 & p6 `1 >= e ) or ( LE p6,q1,P,p1,p2 & p6 `1 >= e ) )per cases
( LE q1,p6,P,p1,p2 or LE p6,q1,P,p1,p2 )
by A11, A5, A21, Th19;
case A22:
LE p6,
q1,
P,
p1,
p2
;
p6 `1 >= e
LE q2,
p6,
P,
p1,
p2
by A16, A20, JORDAN5C:13;
then
p6 in { qq where qq is Point of (TOP-REAL 2) : ( LE q2,qq,P,p1,p2 & LE qq,q1,P,p1,p2 ) }
by A22;
then
p6 in LSeg (
q2,
q1)
by A14, JORDAN6:26;
hence
p6 `1 >= e
by A2, A7, GOBOARD7:5;
verum end; end; end;
hence
p6 `1 >= e
;
verum
end;
p `1 = e
by A2, A4, A7, GOBOARD7:5;
hence
p is_Rout P,
p1,
p2,
e
by A3, A4, A11, A8, A17, A18;
verum end; case A23:
LE q1,
q2,
P,
p1,
p2
;
p is_Rout P,p1,p2,eA24:
now ( ( q1 <> q2 & Segment (P,p1,p2,q1,q2) = LSeg (q1,q2) ) or ( q1 = q2 & Segment (P,p1,p2,q1,q2) = LSeg (q1,q2) ) )per cases
( q1 <> q2 or q1 = q2 )
;
case
q1 <> q2
;
Segment (P,p1,p2,q1,q2) = LSeg (q1,q2)then
LSeg (
q1,
q2)
is_an_arc_of q1,
q2
by TOPREAL1:9;
hence
Segment (
P,
p1,
p2,
q1,
q2)
= LSeg (
q1,
q2)
by A3, A11, A23, Th25;
verum end; end; end; A26:
now not LE p4,q2,P,p1,p2assume
LE p4,
q2,
P,
p1,
p2
;
contradictionthen
p4 in { qq where qq is Point of (TOP-REAL 2) : ( LE q1,qq,P,p1,p2 & LE qq,q2,P,p1,p2 ) }
by A9;
then
p4 in Segment (
P,
p1,
p2,
q1,
q2)
by JORDAN6:26;
hence
contradiction
by A2, A7, A8, A24, GOBOARD7:5;
verum end;
Segment (
P,
p1,
p2,
q1,
q2)
= { p3 where p3 is Point of (TOP-REAL 2) : ( LE q1,p3,P,p1,p2 & LE p3,q2,P,p1,p2 ) }
by JORDAN6:26;
then A27:
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 &
LE q1,
p3,
P,
p1,
p2 &
LE p3,
q2,
P,
p1,
p2 )
by A4, A24;
A28:
for
p6 being
Point of
(TOP-REAL 2) st
LE p6,
p4,
P,
p1,
p2 &
LE p,
p6,
P,
p1,
p2 holds
p6 `1 >= e
proof
let p6 be
Point of
(TOP-REAL 2);
( LE p6,p4,P,p1,p2 & LE p,p6,P,p1,p2 implies p6 `1 >= e )
assume that A29:
LE p6,
p4,
P,
p1,
p2
and A30:
LE p,
p6,
P,
p1,
p2
;
p6 `1 >= e
LE q1,
p6,
P,
p1,
p2
by A27, A30, JORDAN5C:13;
hence
p6 `1 >= e
by A10, A29;
verum
end;
(
LE q2,
p4,
P,
p1,
p2 or
LE p4,
q2,
P,
p1,
p2 )
by A3, A11, A6, A12, Th19;
then A31:
LE p,
p4,
P,
p1,
p2
by A27, A26, JORDAN5C:13;
p `1 = e
by A2, A4, A7, GOBOARD7:5;
hence
p is_Rout P,
p1,
p2,
e
by A3, A4, A11, A8, A31, A28;
verum end; end; end;
hence
p is_Rout P,p1,p2,e
; verum