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 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 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: ( 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 that
A1: q1 is_Rin P,p1,p2,e and
A2: q2 `1 = e and
A3: LSeg (q1,q2) c= P and
A4: p in LSeg (q1,q2) ; :: thesis: p is_Rin 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 p4,q1,P,p1,p2 and
A10: 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;
A11: P is_an_arc_of p1,p2 by A1;
A12: p4 in P by A9, JORDAN5C:def 3;
now :: thesis: ( ( LE q1,q2,P,p1,p2 & p is_Rin P,p1,p2,e ) or ( LE q2,q1,P,p1,p2 & p is_Rin P,p1,p2,e ) )
per cases ( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 ) by A3, A11, A5, A6, Th19;
case A13: LE q1,q2,P,p1,p2 ; :: thesis: p is_Rin P,p1,p2,e
A14: now :: thesis: ( ( 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 ; :: thesis: 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, A13, Th25; :: thesis: verum
end;
case A15: q1 = q2 ; :: thesis: Segment (P,p1,p2,q1,q2) = LSeg (q1,q2)
then LSeg (q1,q2) = {q1} by RLTOPSP1:70;
hence Segment (P,p1,p2,q1,q2) = LSeg (q1,q2) by A11, A5, A15, 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:26;
then A16: 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, A14;
then A17: LE p4,p,P,p1,p2 by A9, JORDAN5C:13;
A18: 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 that
A19: LE p4,p6,P,p1,p2 and
A20: LE p6,p,P,p1,p2 ; :: thesis: p6 `1 >= e
A21: p6 in P by A19, JORDAN5C:def 3;
now :: thesis: ( ( LE p6,q1,P,p1,p2 & p6 `1 >= e ) or ( LE q1,p6,P,p1,p2 & p6 `1 >= e ) )
per cases ( LE p6,q1,P,p1,p2 or LE q1,p6,P,p1,p2 ) by A11, A5, A21, Th19;
case LE p6,q1,P,p1,p2 ; :: thesis: p6 `1 >= e
hence p6 `1 >= e by A10, A19; :: thesis: verum
end;
case A22: LE q1,p6,P,p1,p2 ; :: thesis: p6 `1 >= e
LE p6,q2,P,p1,p2 by A16, A20, 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 A22;
then p6 in LSeg (q1,q2) by A14, JORDAN6:26;
hence p6 `1 >= e by A2, A7, GOBOARD7:5; :: thesis: verum
end;
end;
end;
hence p6 `1 >= e ; :: thesis: verum
end;
p `1 = e by A2, A4, A7, GOBOARD7:5;
hence p is_Rin P,p1,p2,e by A3, A4, A11, A8, A17, A18; :: thesis: verum
end;
case A23: LE q2,q1,P,p1,p2 ; :: thesis: p is_Rin P,p1,p2,e
A24: now :: thesis: ( ( 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 ; :: thesis: 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, A23, Th25; :: thesis: verum
end;
case A25: q1 = q2 ; :: thesis: Segment (P,p1,p2,q2,q1) = LSeg (q2,q1)
then LSeg (q2,q1) = {q1} by RLTOPSP1:70;
hence Segment (P,p1,p2,q2,q1) = LSeg (q2,q1) by A11, A5, A25, Th1; :: thesis: verum
end;
end;
end;
A26: now :: thesis: not LE q2,p4,P,p1,p2
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 A9;
then p4 in Segment (P,p1,p2,q2,q1) by JORDAN6:26;
hence contradiction by A2, A7, A8, A24, GOBOARD7:5; :: thesis: verum
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 A27: 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, A24;
A28: 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 that
A29: LE p4,p6,P,p1,p2 and
A30: LE p6,p,P,p1,p2 ; :: thesis: p6 `1 >= e
LE p6,q1,P,p1,p2 by A27, A30, JORDAN5C:13;
hence p6 `1 >= e by A10, A29; :: thesis: verum
end;
( LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 ) by A3, A11, A6, A12, Th19;
then A31: LE p4,p,P,p1,p2 by A27, A26, JORDAN5C:13;
p `1 = e by A2, A4, A7, GOBOARD7:5;
hence p is_Rin P,p1,p2,e by A3, A4, A11, A8, A31, A28; :: thesis: verum
end;
end;
end;
hence p is_Rin P,p1,p2,e ; :: thesis: verum