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) & q <> 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) & q <> 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 A1: ( p in L~ f & q in L~ f & p <> f . (len f) & q <> f . (len f) & f is being_S-Seq ) ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
then Index p,f < len f by JORDAN3:41;
then A2: ( 1 <= Index p,f & (Index p,f) + 1 <= len f ) by A1, JORDAN3:41, NAT_1:13;
then A3: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by TOPREAL1:def 5;
A4: ( Index p,f in dom f & (Index p,f) + 1 in dom f ) by A2, GOBOARD2:3;
A5: f is one-to-one by A1, TOPREAL1:def 10;
Index p,f < (Index p,f) + 1 by NAT_1:13;
then A6: f /. (Index p,f) <> f /. ((Index p,f) + 1) by A4, A5, 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, JORDAN3:64; :: thesis: verum
end;
suppose A7: Index p,f = Index q,f ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
A8: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A1, A3, JORDAN3:42;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A1, A3, A7, JORDAN3:42;
then A9: ( 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 A6, A8, 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 A9, JORDAN3:def 7;
suppose A10: 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, A7, A10, 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, Th22; :: thesis: verum
end;
end;
end;
end;
suppose A11: 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, A7, A11, 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, 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, JORDAN3:64; :: thesis: verum
end;
end;