let P be non empty Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2, p being Point of (TOP-REAL 2)
for e being Real st p1 `1 < e & p2 `1 > e & q1 is_Rin P,p1,p2,e & q2 `1 = e & LSeg q1,q2 c= P & p in LSeg q1,q2 holds
p is_Rin P,p1,p2,e
let p1, p2, q1, q2, p be Point of (TOP-REAL 2); :: thesis: for e being Real st p1 `1 < e & p2 `1 > e & q1 is_Rin P,p1,p2,e & q2 `1 = e & LSeg q1,q2 c= P & p in LSeg q1,q2 holds
p is_Rin P,p1,p2,e
let e be Real; :: thesis: ( p1 `1 < e & p2 `1 > e & q1 is_Rin P,p1,p2,e & q2 `1 = e & LSeg q1,q2 c= P & p in LSeg q1,q2 implies p is_Rin P,p1,p2,e )
assume A1: ( p1 `1 < e & p2 `1 > e & q1 is_Rin P,p1,p2,e & q2 `1 = e & LSeg q1,q2 c= P & p in LSeg q1,q2 ) ; :: thesis: p is_Rin P,p1,p2,e
then A2: ( P is_an_arc_of p1,p2 & q1 in P & q1 `1 = e & ex p4 being Point of (TOP-REAL 2) st
( p4 `1 > e & LE p4,q1,P,p1,p2 & ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,q1,P,p1,p2 holds
p5 `1 >= e ) ) ) by Def2;
consider p4 being Point of (TOP-REAL 2) such that
A3: ( p4 `1 > e & LE p4,q1,P,p1,p2 & ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,q1,P,p1,p2 holds
p5 `1 >= e ) ) by A1, Def2;
A4: ( q1 in LSeg q1,q2 & q2 in LSeg q1,q2 ) by RLTOPSP1:69;
A5: p4 in P by A3, JORDAN5C:def 3;

now

per cases ( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 ) by A1, A2, A4, Th19;

case A6: LE q1,q2,P,p1,p2 ; :: thesis: p is_Rin P,p1,p2,e

A7: now

per cases ( q1 <> q2 or q1 = q2 ) ;

case q1 <> q2 ; :: thesis: Segment P,p1,p2,q1,q2 = LSeg q1,q2

then LSeg q1,q2 is_an_arc_of q1,q2 by TOPREAL1:15;
hence Segment P,p1,p2,q1,q2 = LSeg q1,q2 by A1, A2, A6, Th28; :: thesis: verum

end;

case A8: q1 = q2 ; :: thesis: Segment P,p1,p2,q1,q2 = LSeg q1,q2

then LSeg q1,q2 = {q1} by RLTOPSP1:71;
hence Segment P,p1,p2,q1,q2 = LSeg q1,q2 by A2, A8, Th1; :: thesis: verum

end;

end;

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:29;
then consider p3 being Point of (TOP-REAL 2) such that
A9: ( p = p3 & LE q1,p3,P,p1,p2 & LE p3,q2,P,p1,p2 ) by A1, A7;
A10: p `1 = e by A1, A2, GOBOARD7:5;
A11: LE p4,p,P,p1,p2 by A3, A9, JORDAN5C:13;
for p6 being Point of (TOP-REAL 2) st LE p4,p6,P,p1,p2 & LE p6,p,P,p1,p2 holds
p6 `1 >= e

proof

let p6 be Point of (TOP-REAL 2); :: thesis: ( LE p4,p6,P,p1,p2 & LE p6,p,P,p1,p2 implies p6 `1 >= e )
assume A12: ( LE p4,p6,P,p1,p2 & LE p6,p,P,p1,p2 ) ; :: thesis: p6 `1 >= e
then A13: p6 in P by JORDAN5C:def 3;

now

per cases ( LE p6,q1,P,p1,p2 or LE q1,p6,P,p1,p2 ) by A2, A13, Th19;

case LE p6,q1,P,p1,p2 ; :: thesis: p6 `1 >= e

hence p6 `1 >= e by A3, A12; :: thesis: verum

end;

case A14: LE q1,p6,P,p1,p2 ; :: thesis: p6 `1 >= e

LE p6,q2,P,p1,p2 by A9, A12, JORDAN5C:13;
then p6 in { qq where qq is Point of (TOP-REAL 2) : ( LE q1,qq,P,p1,p2 & LE qq,q2,P,p1,p2 ) } by A14;
then p6 in LSeg q1,q2 by A7, JORDAN6:29;
hence p6 `1 >= e by A1, A2, GOBOARD7:5; :: thesis: verum

end;

end;

end;

hence p6 `1 >= e ; :: thesis: verum

end;

hence p is_Rin P,p1,p2,e by A1, A2, A3, A10, A11, Def2; :: thesis: verum

end;

case A15: LE q2,q1,P,p1,p2 ; :: thesis: p is_Rin P,p1,p2,e

A16: now

per cases ( q1 <> q2 or q1 = q2 ) ;

case q1 <> q2 ; :: thesis: Segment P,p1,p2,q2,q1 = LSeg q2,q1

then LSeg q2,q1 is_an_arc_of q2,q1 by TOPREAL1:15;
hence Segment P,p1,p2,q2,q1 = LSeg q2,q1 by A1, A2, A15, Th28; :: thesis: verum

end;

case A17: q1 = q2 ; :: thesis: Segment P,p1,p2,q2,q1 = LSeg q2,q1

then LSeg q2,q1 = {q1} by RLTOPSP1:71;
hence Segment P,p1,p2,q2,q1 = LSeg q2,q1 by A2, A17, Th1; :: thesis: 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:29;
then consider p3 being Point of (TOP-REAL 2) such that
A18: ( p = p3 & LE q2,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) by A1, A16;
A19: p `1 = e by A1, A2, GOBOARD7:5;
A20: ( LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 ) by A1, A2, A4, A5, Th19;

now

assume LE q2,p4,P,p1,p2 ; :: thesis: contradiction
then p4 in { qq where qq is Point of (TOP-REAL 2) : ( LE q2,qq,P,p1,p2 & LE qq,q1,P,p1,p2 ) } by A3;
then p4 in Segment P,p1,p2,q2,q1 by JORDAN6:29;
hence contradiction by A1, A2, A3, A16, GOBOARD7:5; :: thesis: verum

end;

then A21: LE p4,p,P,p1,p2 by A18, A20, JORDAN5C:13;
for p6 being Point of (TOP-REAL 2) st LE p4,p6,P,p1,p2 & LE p6,p,P,p1,p2 holds
p6 `1 >= e

proof

let p6 be Point of (TOP-REAL 2); :: thesis: ( LE p4,p6,P,p1,p2 & LE p6,p,P,p1,p2 implies p6 `1 >= e )
assume A22: ( LE p4,p6,P,p1,p2 & LE p6,p,P,p1,p2 ) ; :: thesis: p6 `1 >= e
then LE p6,q1,P,p1,p2 by A18, JORDAN5C:13;
hence p6 `1 >= e by A3, A22; :: thesis: verum

end;

hence p is_Rin P,p1,p2,e by A1, A2, A3, A19, A21, Def2; :: thesis: verum

end;

end;

end;

hence p is_Rin P,p1,p2,e ; :: thesis: verum