let f be V26() standard special_circular_sequence; (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 ;
TARSKI:def 3 ( 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)))
;
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 ( ( 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
;
contradictionnow ( ( 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)))
;
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;
verum end; case A25:
f /. ((len f) -' 1) in LSeg (
(f /. 1),
(f /. (1 + 1)))
;
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;
verum end; hence
contradiction
;
verum
hence
x in {(f . 1)}
;
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; verum