let f be non constant standard special_circular_sequence; :: thesis: (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)}
A1:
3 < len f
by GOBOARD7:36, XXREAL_0:2;
A2:
len f > 4
by GOBOARD7:36;
then A3:
(len f) - 1 = (len f) -' 1
by XREAL_1:235, XXREAL_0:2;
A4:
2 < len f
by GOBOARD7:36, XXREAL_0:2;
then A5:
(1 + 1) - 1 <= (len f) - 1
by XREAL_1:11;
((len f) - 1) + 1 = len f
;
then A6:
f /. (len f) in LSeg f,((len f) -' 1)
by A3, A5, TOPREAL1:27;
A7:
f /. 1 = f /. (len f)
by FINSEQ_6:def 1;
A8:
1 < len f
by GOBOARD7:36, XXREAL_0:2;
A9:
(3 + 1) - 1 < (len f) - 1
by A2, XREAL_1:11;
A10:
(LSeg f,1) /\ (LSeg f,((len f) -' 1)) c= {(f . 1)}
proof
let x be
set ;
:: 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:36, 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 5;
(2 + 1) - 1
<= (len f) - 1
by A1, XREAL_1:11;
then A14:
(1 + 1) - 1
<= ((len f) -' 1) - 1
by A3, XREAL_1:11;
A15:
LSeg (f /. 1),
(f /. (1 + 1)) = LSeg f,1
by A4, TOPREAL1:def 5;
((len f) -' 1) + 1 =
((len f) - 1) + 1
by A2, XREAL_1:235, 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 5;
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 5;
len f < (len f) + 1
by NAT_1:13;
then A19:
(len f) - 1
< ((len f) + 1) - 1
by XREAL_1:11;
(((len f) -' 1) -' 1) + 1 =
(((len f) -' 1) - 1) + 1
by A3, A5, XREAL_1:235
.=
(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 5;
A21:
LSeg (f /. ((len f) -' 1)),
(f /. (((len f) -' 1) + 1)) = LSeg f,
((len f) -' 1)
by A3, A5, TOPREAL1:def 5;
now per cases
( p <> f /. 1 or p = f /. 1 )
;
case A22:
p <> f /. 1
;
:: thesis: contradictionnow 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, Th53;
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:235, 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:69;
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:69;
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:11;
then
(2 + 1) - 1
< ((len f) - 1) - 1
by XREAL_1:11;
then A27:
1
+ 1
< ((len f) -' 1) -' 1
by A3, A5, XREAL_1:235;
(((len f) - 1) - 1) + 1
< len f
by A19;
then
(((len f) -' 1) -' 1) + 1
< len f
by A3, A5, XREAL_1:235;
hence
contradiction
by A26, A27, GOBOARD5:def 4;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum
hence
x in {(f . 1)}
;
:: thesis: verum
end;
1 + 1 <= len f
by GOBOARD7:36, XXREAL_0:2;
then A28:
f /. 1 in LSeg f,1
by TOPREAL1:27;
f . 1 = f /. 1
by A8, FINSEQ_4:24;
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:37;
hence
(LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)}
by A10, XBOOLE_0:def 10; :: thesis: verum