let f be circular unfolded s.c.c. FinSequence of (TOP-REAL 2); :: thesis: ( len f > 4 implies (LSeg f,1) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)} )
assume A1:
len f > 4
; :: thesis: (LSeg f,1) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}
A2:
1 < len f
by A1, 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) ) } ;
set h2 = f /^ 1;
A3:
1 + 2 <= len f
by A1, XXREAL_0:2;
A4:
1 <= len f
by A1, XXREAL_0:2;
then A5: (LSeg f,1) /\ (LSeg (f /^ 1),1) =
(LSeg f,1) /\ (LSeg f,(1 + 1))
by SPPOL_2:4
.=
{(f /. (1 + 1))}
by A3, TOPREAL1:def 8
;
A6:
len (f /^ 1) = (len f) - 1
by A4, RFINSEQ:def 2;
then A7:
(len (f /^ 1)) + 1 = len f
;
len f > 3 + 1
by A1;
then A8:
len (f /^ 1) > 2 + 1
by A7, XREAL_1:8;
then A9:
1 + 1 <= len (f /^ 1)
by NAT_1:13;
A10:
1 + 1 <= len (f /^ 1)
by A8, XXREAL_0:2;
then A11:
1 <= (len (f /^ 1)) -' 1
by NAT_D:55;
A12: 1 + ((len (f /^ 1)) -' 1) =
len (f /^ 1)
by A8, XREAL_1:237, XXREAL_0:2
.=
(len f) -' 1
by A1, A6, XREAL_1:235, XXREAL_0:2
;
A13:
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) ) } )
LSeg (f /^ 1),1 in { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ 1) ) }
by A9;
then A19:
LSeg (f /^ 1),1 c= L~ (f /^ 1)
by ZFMISC_1:92;
((len (f /^ 1)) -' 1) + 1 <= len (f /^ 1)
by A8, XREAL_1:237, XXREAL_0:2;
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 A11;
then
LSeg (f /^ 1),((len (f /^ 1)) -' 1) c= L~ (f /^ 1)
by ZFMISC_1:92;
then A20:
(LSeg (f /^ 1),1) \/ (LSeg (f /^ 1),((len (f /^ 1)) -' 1)) c= L~ (f /^ 1)
by A19, XBOOLE_1:8;
union { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) } c= L~ (f /^ 1)
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 A20, XBOOLE_1:8;
then A23:
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 A13, XBOOLE_0:def 10;
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 ;
:: thesis: ( 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 ) )
:: thesis: ( 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 A24:
Z in {{} }
;
:: thesis: 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;
:: thesis: 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);
:: thesis: ( 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;
:: thesis: ( 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 A4, SPPOL_2:4;
hence
Y in { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) }
by A8;
:: thesis: Z = X /\ Y
A25:
1
+ 1
< 3
;
3
+ 1
< len f
by A1;
then
X misses Y
by A25, GOBOARD5:def 4;
then
X /\ Y = {}
by XBOOLE_0:def 7;
hence
Z = X /\ Y
by A24, TARSKI:def 1;
:: thesis: verum
end;
given X,
Y being
set such that A26:
X in {(LSeg f,1)}
and A27:
Y in { (LSeg (f /^ 1),i) where i is Element of NAT : ( 1 < i & i + 1 < len (f /^ 1) ) }
and A28:
Z = X /\ Y
;
:: thesis: Z in {{} }
A29:
X = LSeg f,1
by A26, TARSKI:def 1;
consider i being
Element of
NAT such that A30:
Y = LSeg (f /^ 1),
i
and A31:
1
< i
and A32:
i + 1
< len (f /^ 1)
by A27;
A33:
LSeg (f /^ 1),
i = LSeg f,
(i + 1)
by A2, A31, SPPOL_2:4;
A34:
(i + 1) + 1
< len f
by A7, A32, XREAL_1:8;
1
+ 1
< i + 1
by A31, XREAL_1:8;
then
X misses Y
by A29, A30, A33, A34, GOBOARD5:def 4;
then
Z = {}
by A28, XBOOLE_0:def 7;
hence
Z in {{} }
by TARSKI:def 1;
:: thesis: 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 A35: (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
;
A36: (LSeg f,1) /\ (LSeg (f /^ 1),((len (f /^ 1)) -' 1)) =
(LSeg f,1) /\ (LSeg f,((len f) -' 1))
by A4, A10, A12, NAT_D:55, SPPOL_2:4
.=
{(f /. 1)}
by A1, REVROT_1:30
;
thus (LSeg f,1) /\ (L~ (f /^ 1)) =
((LSeg f,1) /\ ((LSeg (f /^ 1),1) \/ (LSeg (f /^ 1),((len (f /^ 1)) -' 1)))) \/ {}
by A23, A35, XBOOLE_1:23
.=
{(f /. 1)} \/ {(f /. 2)}
by A5, A36, XBOOLE_1:23
.=
{(f /. 1),(f /. 2)}
by ENUMSET1:41
; :: thesis: verum