let f be constant standard special_circular_sequence; :: thesis: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)}
A1: 3 < len f by GOBOARD7:34, XXREAL_0:2;
A2: len f > 4 by GOBOARD7:34;
then A3: (len f) - 1 = (len f) -' 1 by XREAL_1:233, XXREAL_0:2;
A4: 2 < len f by GOBOARD7:34, XXREAL_0:2;
then A5: (1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
((len f) - 1) + 1 = len f ;
then A6: f /. (len f) in LSeg (f,((len f) -' 1)) by A3, A5, TOPREAL1:21;
A7: f /. 1 = f /. (len f) by FINSEQ_6:def 1;
A8: 1 < len f by GOBOARD7:34, XXREAL_0:2;
A9: (3 + 1) - 1 < (len f) - 1 by A2, XREAL_1:9;
A10: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) c= {(f . 1)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) or x in {(f . 1)} )
A11: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
assume A12: x in (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) ; :: thesis: x in {(f . 1)}
then reconsider p = x as Point of (TOP-REAL 2) ;
x in LSeg (f,1) by A12, XBOOLE_0:def 4;
then A13: p in LSeg ((f /. 1),(f /. (1 + 1))) by A11, TOPREAL1:def 3;
(2 + 1) - 1 <= (len f) - 1 by A1, XREAL_1:9;
then A14: (1 + 1) - 1 <= ((len f) -' 1) - 1 by A3, XREAL_1:9;
A15: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,1) by A4, TOPREAL1:def 3;
((len f) -' 1) + 1 = ((len f) - 1) + 1 by A2, XREAL_1:233, XXREAL_0:2
.= len f ;
then A16: f /. (((len f) -' 1) + 1) = f /. 1 by FINSEQ_6:def 1;
A17: LSeg ((f /. (1 + 1)),(f /. ((1 + 1) + 1))) = LSeg (f,(1 + 1)) by A1, TOPREAL1:def 3;
x in LSeg (f,((len f) -' 1)) by A12, XBOOLE_0:def 4;
then A18: p in LSeg ((f /. 1),(f /. ((len f) -' 1))) by A3, A5, A16, TOPREAL1:def 3;
len f < (len f) + 1 by NAT_1:13;
then A19: (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:9;
(((len f) -' 1) -' 1) + 1 = (((len f) -' 1) - 1) + 1 by A3, A5, XREAL_1:233
.= (len f) -' 1 ;
then A20: LSeg ((f /. (((len f) -' 1) -' 1)),(f /. ((len f) -' 1))) = LSeg (f,(((len f) -' 1) -' 1)) by A3, A14, A19, TOPREAL1:def 3;
A21: LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) = LSeg (f,((len f) -' 1)) by A3, A5, TOPREAL1:def 3;

now :: thesis: ( ( p <> f /. 1 & contradiction ) or ( p = f /. 1 & x in {(f . 1)} ) )

per cases ( p <> f /. 1 or p = f /. 1 ) ;

case A22: p <> f /. 1 ; :: thesis: contradiction

now :: thesis: ( ( f /. (1 + 1) in LSeg ((f /. 1),(f /. ((len f) -' 1))) & contradiction ) or ( f /. ((len f) -' 1) in LSeg ((f /. 1),(f /. (1 + 1))) & contradiction ) )

per cases ( f /. (1 + 1) in LSeg ((f /. 1),(f /. ((len f) -' 1))) or f /. ((len f) -' 1) in LSeg ((f /. 1),(f /. (1 + 1))) ) by A13, A18, A22, Th41;

case A23: f /. (1 + 1) in LSeg ((f /. 1),(f /. ((len f) -' 1))) ; :: thesis: contradiction

((len f) -' 1) + 1 = ((len f) - 1) + 1 by A2, XREAL_1:233, XXREAL_0:2
.= len f ;
then A24: f /. (((len f) -' 1) + 1) = f /. 1 by FINSEQ_6:def 1;
f /. (1 + 1) in LSeg ((f /. (1 + 1)),(f /. ((1 + 1) + 1))) by RLTOPSP1:68;
then (LSeg ((f /. (1 + 1)),(f /. ((1 + 1) + 1)))) /\ (LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1)))) <> {} by A23, A24, XBOOLE_0:def 4;
then LSeg ((f /. (1 + 1)),(f /. ((1 + 1) + 1))) meets LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by XBOOLE_0:def 7;
hence contradiction by A9, A3, A17, A19, A21, GOBOARD5:def 4; :: thesis: verum

end;

case A25: f /. ((len f) -' 1) in LSeg ((f /. 1),(f /. (1 + 1))) ; :: thesis: contradiction

f /. ((len f) -' 1) in LSeg ((f /. (((len f) -' 1) -' 1)),(f /. ((len f) -' 1))) by RLTOPSP1:68;
then (LSeg (f,1)) /\ (LSeg (f,(((len f) -' 1) -' 1))) <> {} by A15, A20, A25, XBOOLE_0:def 4;
then A26: LSeg (f,1) meets LSeg (f,(((len f) -' 1) -' 1)) by XBOOLE_0:def 7;
(3 + 1) - 1 < (len f) - 1 by A2, XREAL_1:9;
then (2 + 1) - 1 < ((len f) - 1) - 1 by XREAL_1:9;
then A27: 1 + 1 < ((len f) -' 1) -' 1 by A3, A5, XREAL_1:233;
(((len f) - 1) - 1) + 1 < len f by A19;
then (((len f) -' 1) -' 1) + 1 < len f by A3, A5, XREAL_1:233;
hence contradiction by A26, A27, GOBOARD5:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case p = f /. 1 ; :: thesis: x in {(f . 1)}

then x in {(f /. 1)} by TARSKI:def 1;
hence x in {(f . 1)} by A8, FINSEQ_4:15; :: thesis: verum

end;

end;

end;

hence x in {(f . 1)} ; :: thesis: verum

end;

1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A28: f /. 1 in LSeg (f,1) by TOPREAL1:21;
f . 1 = f /. 1 by A8, FINSEQ_4:15;
then f . 1 in (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) by A28, A6, A7, XBOOLE_0:def 4;
then {(f . 1)} c= (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) by ZFMISC_1:31;
hence (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by A10, XBOOLE_0:def 10; :: thesis: verum