let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p <> f . (len f) & p in L~ f & q in L~ 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 <> f . (len f) & p in L~ f & q in L~ 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 <> f . (len f) ; :: thesis: ( not p in L~ f or not q in L~ f or not f is being_S-Seq or p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )
assume A2: ( p in L~ f & q in L~ f & f is being_S-Seq ) ; :: thesis: ( p in L~ (L_Cut f,q) or q in L~ (L_Cut f,p) )

per cases ( ( p <> f . (len f) & q = f . (len f) ) or ( p = f . (len f) & q <> f . (len f) ) or ( p <> f . (len f) & q <> f . (len f) ) ) by A1;

suppose ( p <> f . (len f) & q = f . (len 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 A2, Th25; :: thesis: verum

end;

suppose ( p = f . (len f) & q <> f . (len 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 A2, Th25; :: thesis: verum

end;

suppose ( p <> f . (len f) & q <> f . (len 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 A2, Lm3; :: thesis: verum

end;

end;