let f be circular unfolded s.c.c. FinSequence of (TOP-REAL 2); ( len f > 4 implies (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)} )
assume A1:
len f > 4
; (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}
A2:
1 + 2 <= len f
by A1, XXREAL_0:2;
set h2 = f /^ 1;
A3:
1 <= len f
by A1, XXREAL_0:2;
then A4:
len (f /^ 1) = (len f) - 1
by RFINSEQ:def 1;
then A5:
(len (f /^ 1)) + 1 = len f
;
len f > 3 + 1
by A1;
then A6:
len (f /^ 1) > 2 + 1
by A5, XREAL_1:6;
then A7:
1 + 1 <= len (f /^ 1)
by XXREAL_0:2;
set SFY = { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ;
set Reszta = union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ;
A8:
((len (f /^ 1)) -' 1) + 1 <= len (f /^ 1)
by A6, XREAL_1:235, XXREAL_0:2;
A9:
1 < len f
by A1, XXREAL_0:2;
for Z being set holds
( Z in {{}} iff ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) )
proof
let Z be
set ;
( Z in {{}} iff ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) )
thus
(
Z in {{}} implies ex
X,
Y being
set st
(
X in {(LSeg (f,1))} &
Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } &
Z = X /\ Y ) )
( ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) implies Z in {{}} )proof
assume A10:
Z in {{}}
;
ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
take X =
LSeg (
f,1);
ex Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
take Y =
LSeg (
f,
(2 + 1));
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
thus
X in {(LSeg (f,1))}
by TARSKI:def 1;
( Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
Y = LSeg (
(f /^ 1),2)
by A3, SPPOL_2:4;
hence
Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) }
by A6;
Z = X /\ Y
A11:
1
+ 1
< 3
;
3
+ 1
< len f
by A1;
then
X misses Y
by A11, GOBOARD5:def 4;
then
X /\ Y = {}
by XBOOLE_0:def 7;
hence
Z = X /\ Y
by A10, TARSKI:def 1;
verum
end;
given X,
Y being
set such that A12:
X in {(LSeg (f,1))}
and A13:
Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) }
and A14:
Z = X /\ Y
;
Z in {{}}
A15:
X = LSeg (
f,1)
by A12, TARSKI:def 1;
consider i being
Nat such that A16:
Y = LSeg (
(f /^ 1),
i)
and A17:
1
< i
and A18:
i + 1
< len (f /^ 1)
by A13;
A19:
1
+ 1
< i + 1
by A17, XREAL_1:6;
A20:
(i + 1) + 1
< len f
by A5, A18, XREAL_1:6;
LSeg (
(f /^ 1),
i)
= LSeg (
f,
(i + 1))
by A9, A17, SPPOL_2:4;
then
X misses Y
by A15, A16, A20, A19, GOBOARD5:def 4;
then
Z = {}
by A14, XBOOLE_0:def 7;
hence
Z in {{}}
by TARSKI:def 1;
verum
end;
then
INTERSECTION ({(LSeg (f,1))}, { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) = {{}}
by SETFAM_1:def 5;
then A21: (LSeg (f,1)) /\ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) =
union {{}}
by SETFAM_1:25
.=
{}
by ZFMISC_1:25
;
A22:
L~ (f /^ 1) c= ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
A28:
union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } c= L~ (f /^ 1)
1 + ((len (f /^ 1)) -' 1) =
len (f /^ 1)
by A6, XREAL_1:235, XXREAL_0:2
.=
(len f) -' 1
by A1, A4, XREAL_1:233, XXREAL_0:2
;
then A31: (LSeg (f,1)) /\ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) =
(LSeg (f,1)) /\ (LSeg (f,((len f) -' 1)))
by A3, A7, NAT_D:55, SPPOL_2:4
.=
{(f /. 1)}
by A1, REVROT_1:30
;
1 + 1 <= len (f /^ 1)
by A6, NAT_1:13;
then
LSeg ((f /^ 1),1) in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ 1) ) }
;
then A32:
LSeg ((f /^ 1),1) c= L~ (f /^ 1)
by ZFMISC_1:74;
A33: (LSeg (f,1)) /\ (LSeg ((f /^ 1),1)) =
(LSeg (f,1)) /\ (LSeg (f,(1 + 1)))
by A3, SPPOL_2:4
.=
{(f /. (1 + 1))}
by A2, TOPREAL1:def 6
;
1 <= (len (f /^ 1)) -' 1
by A7, NAT_D:55;
then
LSeg ((f /^ 1),((len (f /^ 1)) -' 1)) in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ 1) ) }
by A8;
then
LSeg ((f /^ 1),((len (f /^ 1)) -' 1)) c= L~ (f /^ 1)
by ZFMISC_1:74;
then
(LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) c= L~ (f /^ 1)
by A32, XBOOLE_1:8;
then
((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) c= L~ (f /^ 1)
by A28, XBOOLE_1:8;
then
L~ (f /^ 1) = ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
by A22, XBOOLE_0:def 10;
hence (LSeg (f,1)) /\ (L~ (f /^ 1)) =
((LSeg (f,1)) /\ ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))))) \/ {}
by A21, XBOOLE_1:23
.=
{(f /. 1)} \/ {(f /. 2)}
by A33, A31, XBOOLE_1:23
.=
{(f /. 1),(f /. 2)}
by ENUMSET1:1
;
verum