let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut f,q) holds
q in L~ (L_Cut f,p)
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut f,q) implies q in L~ (L_Cut f,p) )
assume that
A1: p in L~ f and
A2: q in L~ f and
A3: p <> f . (len f) and
A4: f is being_S-Seq ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
A5: Index p,f < len f by A1, JORDAN3:41;
A6: 1 <= Index p,f by A1, JORDAN3:41;
A7: (Index p,f) + 1 <= len f by A5, NAT_1:13;
then A8: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A6, TOPREAL1:def 5;
A9: Index p,f in dom f by A6, A7, SEQ_4:151;
A10: (Index p,f) + 1 in dom f by A6, A7, SEQ_4:151;
A11: f is one-to-one by A4, TOPREAL1:def 10;
Index p,f < (Index p,f) + 1 by NAT_1:13;
then A12: f /. (Index p,f) <> f /. ((Index p,f) + 1) by A9, A10, A11, PARTFUN2:17;
per cases ( Index p,f < Index q,f or Index p,f = Index q,f or Index p,f > Index q,f ) by XXREAL_0:1;
suppose Index p,f < Index q,f ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) by A1, A2, JORDAN3:64; :: thesis: verum
end;
suppose A13: Index p,f = Index q,f ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
A14: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A1, A8, JORDAN3:42;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, A8, A13, JORDAN3:42;
then A15: ( LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) or LT q,p,f /. (Index p,f),f /. ((Index p,f) + 1) ) by A12, A14, JORDAN3:63;
now
per cases ( LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) or LE q,p,f /. (Index p,f),f /. ((Index p,f) + 1) ) by A15, JORDAN3:def 7;
suppose A16: LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
thus ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) :: thesis: verum
proof
per cases ( p <> q or p = q ) ;
suppose p <> q ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) by A1, A2, A13, A16, JORDAN3:66; :: thesis: verum
end;
suppose p = q ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) by A1, A3, A4, Th22; :: thesis: verum
end;
end;
end;
end;
suppose A17: LE q,p,f /. (Index p,f),f /. ((Index p,f) + 1) ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
thus ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) :: thesis: verum
proof
per cases ( p <> q or p = q ) ;
suppose p <> q ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) by A1, A2, A13, A17, JORDAN3:66; :: thesis: verum
end;
suppose p = q ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) by A1, A3, A4, Th22; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) ; :: thesis: verum
end;
suppose Index p,f > Index q,f ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
hence ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) ) by A1, A2, JORDAN3:64; :: thesis: verum
end;
end;