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 that
A2: p in L~ f and
A3: q in L~ f and
A4: 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, A3, A4, Th22; :: 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, A3, A4, Th22; :: 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, A3, A4, Lm2; :: thesis: verum
end;
end;