let f be circular unfolded s.c.c. FinSequence of ; ( 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 2;
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:8;
then A7:
1 + 1 <= len (f /^ 1)
by XXREAL_0:2;
set SFY = { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ;
set Reszta = union { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ;
A8:
((len (f /^ 1)) -' 1) + 1 <= len (f /^ 1)
by A6, XREAL_1:237, 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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
Element of
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:8;
A20:
(i + 1) + 1
< len f
by A5, A18, XREAL_1:8;
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 Element of 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 Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } ) =
union {{} }
by SETFAM_1:36
.=
{}
by ZFMISC_1:31
;
A22:
L~ (f /^ 1) c= ((LSeg (f /^ 1),1) \/ (LSeg (f /^ 1),((len (f /^ 1)) -' 1))) \/ (union { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } )
A28:
union { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } c= L~ (f /^ 1)
1 + ((len (f /^ 1)) -' 1) =
len (f /^ 1)
by A6, XREAL_1:237, XXREAL_0:2
.=
(len f) -' 1
by A1, A4, XREAL_1:235, 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 Element of NAT : ( 1 <= i & i + 1 <= len (f /^ 1) ) }
;
then A32:
LSeg (f /^ 1),1 c= L~ (f /^ 1)
by ZFMISC_1:92;
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 8
;
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 Element of 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:92;
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 Element of 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 Element of 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:41
;
verum