let f be non constant standard special_circular_sequence; :: thesis: (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)}
A1:
len f > 4
by GOBOARD7:36;
A2:
2 < len f
by GOBOARD7:36, XXREAL_0:2;
A3:
3 < len f
by GOBOARD7:36, XXREAL_0:2;
A4:
(3 + 1) - 1 < (len f) - 1
by A1, XREAL_1:11;
( 1 <= 1 & 1 + 1 <= len f )
by GOBOARD7:36, XXREAL_0:2;
then A5:
f /. 1 in LSeg f,1
by TOPREAL1:27;
A6:
1 < len f
by GOBOARD7:36, XXREAL_0:2;
A7:
(len f) - 1 = (len f) -' 1
by A1, XREAL_1:235, XXREAL_0:2;
A8:
(1 + 1) - 1 <= (len f) - 1
by A2, XREAL_1:11;
((len f) - 1) + 1 = len f
;
then A9:
f /. (len f) in LSeg f,((len f) -' 1)
by A7, A8, TOPREAL1:27;
A10:
f . 1 = f /. 1
by A6, FINSEQ_4:24;
f /. 1 = f /. (len f)
by FINSEQ_6:def 1;
then
f . 1 in (LSeg f,1) /\ (LSeg f,((len f) -' 1))
by A5, A9, A10, XBOOLE_0:def 4;
then A11:
{(f . 1)} c= (LSeg f,1) /\ (LSeg f,((len f) -' 1))
by ZFMISC_1:37;
(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)} )
assume A12:
x in (LSeg f,1) /\ (LSeg f,((len f) -' 1))
;
:: thesis: x in {(f . 1)}
then A13:
(
x in LSeg f,1 &
x in LSeg f,
((len f) -' 1) )
by XBOOLE_0:def 4;
reconsider p =
x as
Point of
(TOP-REAL 2) by A12;
A14:
1
+ 1
<= len f
by GOBOARD7:36, XXREAL_0:2;
A15:
LSeg (f /. 1),
(f /. (1 + 1)) = LSeg f,1
by A2, TOPREAL1:def 5;
A16:
LSeg (f /. (1 + 1)),
(f /. ((1 + 1) + 1)) = LSeg f,
(1 + 1)
by A3, TOPREAL1:def 5;
A17:
p in LSeg (f /. 1),
(f /. (1 + 1))
by A13, A14, TOPREAL1:def 5;
((len f) -' 1) + 1 =
((len f) - 1) + 1
by A1, XREAL_1:235, XXREAL_0:2
.=
len f
;
then
f /. (((len f) -' 1) + 1) = f /. 1
by FINSEQ_6:def 1;
then A18:
p in LSeg (f /. 1),
(f /. ((len f) -' 1))
by A7, A8, A13, TOPREAL1:def 5;
(2 + 1) - 1
<= (len f) - 1
by A3, XREAL_1:11;
then A19:
(1 + 1) - 1
<= ((len f) -' 1) - 1
by A7, XREAL_1:11;
len f < (len f) + 1
by NAT_1:13;
then A20:
(len f) - 1
< ((len f) + 1) - 1
by XREAL_1:11;
(((len f) -' 1) -' 1) + 1 =
(((len f) -' 1) - 1) + 1
by A7, A8, XREAL_1:235
.=
(len f) -' 1
;
then A21:
LSeg (f /. (((len f) -' 1) -' 1)),
(f /. ((len f) -' 1)) = LSeg f,
(((len f) -' 1) -' 1)
by A7, A19, A20, TOPREAL1:def 5;
A22:
LSeg (f /. ((len f) -' 1)),
(f /. (((len f) -' 1) + 1)) = LSeg f,
((len f) -' 1)
by A7, A8, TOPREAL1:def 5;
now per cases
( p <> f /. 1 or p = f /. 1 )
;
case A23:
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 A17, A18, A23, Th53;
case A24:
f /. (1 + 1) in LSeg (f /. 1),
(f /. ((len f) -' 1))
;
:: thesis: contradiction((len f) -' 1) + 1 =
((len f) - 1) + 1
by A1, XREAL_1:235, XXREAL_0:2
.=
len f
;
then A25:
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 A24, A25, 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 A4, A7, A16, A20, A22, GOBOARD5:def 4;
:: thesis: verum end; case A26:
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, A21, A26, XBOOLE_0:def 4;
then A27:
LSeg f,1
meets LSeg f,
(((len f) -' 1) -' 1)
by XBOOLE_0:def 7;
(3 + 1) - 1
< (len f) - 1
by A1, XREAL_1:11;
then A28:
(2 + 1) - 1
< ((len f) - 1) - 1
by XREAL_1:11;
(((len f) - 1) - 1) + 1
< len f
by A20;
then
( 1
+ 1
< ((len f) -' 1) -' 1 &
(((len f) -' 1) -' 1) + 1
< len f )
by A7, A8, A28, XREAL_1:235;
hence
contradiction
by A27, GOBOARD5:def 4;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum
hence
x in {(f . 1)}
;
:: thesis: verum
end;
hence
(LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)}
by A11, XBOOLE_0:def 10; :: thesis: verum