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:237, 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)} by SUBSET_1:7;
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 5;
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:20;

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:27;
3 + 1 = 4 ;
then (1 + 1) + 1 < (len f) - 1 by A1, XREAL_1:22;
then A13: (1 + 1) + 1 < (len f) -' 1 by A1, XREAL_1:235, 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:237 ;
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:22;
then 1 + 1 < (len f) -' 2 by A1, XREAL_1:235, 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:21;
then 1 <= (len f) -' 2 by NAT_D:39;
then f /. ((len f) -' 1) in LSeg f,((len f) -' 2) by A15, A16, TOPREAL1:27;
hence contradiction by A14, A17, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

let x be set ; :: 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:27;
x in LSeg f,1 by A3, A18, TOPREAL1:27;
hence x in (LSeg f,((len f) -' 1)) /\ (LSeg f,1) by A19, XBOOLE_0:def 4; :: thesis: verum