let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: ( len f > 4 implies (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) = {(f /. 1)} )
assume A1: len f > 4 ; :: thesis: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) = {(f /. 1)}
then A2: ((len f) -' 1) + 1 = len f by XREAL_1:235, XXREAL_0:2;
A3: len f >= 1 + 1 by A1, XXREAL_0:2;
then A4: 1 <= (len f) -' 1 by NAT_D:55;
A5: len f >= (1 + 1) + 1 by A1, XXREAL_0:2;
thus (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) c= {(f /. 1)} :: according to XBOOLE_0:def 10 :: thesis: {(f /. 1)} c= (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1))
proof
assume not (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) c= {(f /. 1)} ; :: thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A6: p in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) and
A7: not p in {(f /. 1)} ;
A8: p <> f /. 1 by A7, TARSKI:def 1;
A9: ( LSeg (f,((len f) -' 1)) = LSeg ((f /. ((len f) -' 1)),(f /. (len f))) & LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) ) by A3, A2, A4, TOPREAL1:def 3;
A10: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
per cases ( f /. (1 + 1) in LSeg (f,((len f) -' 1)) or f /. ((len f) -' 1) in LSeg (f,1) ) by A6, A9, A8, A10, JGRAPH_1:16;
suppose A11: f /. (1 + 1) in LSeg (f,((len f) -' 1)) ; :: thesis: contradiction
A12: f /. (1 + 1) in LSeg (f,(1 + 1)) by A5, TOPREAL1:21;
3 + 1 = 4 ;
then (1 + 1) + 1 < (len f) - 1 by A1, XREAL_1:20;
then A13: (1 + 1) + 1 < (len f) -' 1 by A1, XREAL_1:233, XXREAL_0:2;
(len f) -' 1 < len f by A4, NAT_D:51;
then LSeg (f,(1 + 1)) misses LSeg (f,((len f) -' 1)) by A13, GOBOARD5:def 4;
hence contradiction by A11, A12, XBOOLE_0:3; :: thesis: verum
end;
suppose A14: f /. ((len f) -' 1) in LSeg (f,1) ; :: thesis: contradiction
A15: ((len f) -' 2) + 1 = (((len f) -' 1) -' 1) + 1 by NAT_D:45
.= (len f) -' 1 by A3, NAT_D:55, XREAL_1:235 ;
then A16: ((len f) -' 2) + 1 < len f by A4, NAT_D:51;
2 + 2 < len f by A1;
then 1 + 1 < (len f) - 2 by XREAL_1:20;
then 1 + 1 < (len f) -' 2 by A1, XREAL_1:233, XXREAL_0:2;
then A17: LSeg (f,1) misses LSeg (f,((len f) -' 2)) by A16, GOBOARD5:def 4;
1 <= (len f) - 2 by A5, XREAL_1:19;
then 1 <= (len f) -' 2 by NAT_D:39;
then f /. ((len f) -' 1) in LSeg (f,((len f) -' 2)) by A15, A16, TOPREAL1:21;
hence contradiction by A14, A17, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f /. 1)} or x in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) )
assume x in {(f /. 1)} ; :: thesis: x in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1))
then A18: x = f /. 1 by TARSKI:def 1;
then x = f /. (len f) by FINSEQ_6:def 1;
then A19: x in LSeg (f,((len f) -' 1)) by A2, A4, TOPREAL1:21;
x in LSeg (f,1) by A3, A18, TOPREAL1:21;
hence x in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) by A19, XBOOLE_0:def 4; :: thesis: verum