let i, j, m, n be Nat; for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds
L~ (mid (f,i,j)) misses L~ (mid (f,m,n))
let f be V22() standard special_circular_sequence; ( 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) implies L~ (mid (f,i,j)) misses L~ (mid (f,m,n)) )
assume that
A1:
( 1 <= i & i <= j )
and
A2:
j < m
and
A3:
m <= n
and
A4:
n <= len f
and
A5:
( 1 < i or n < len f )
; L~ (mid (f,i,j)) misses L~ (mid (f,m,n))
set A = { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } ;
set B = { (LSeg (f,l)) where l is Nat : ( m <= l & l < n ) } ;
1 <= j
by A1, XXREAL_0:2;
then
1 < m
by A2, XXREAL_0:2;
then A6:
L~ (mid (f,m,n)) = union { (LSeg (f,l)) where l is Nat : ( m <= l & l < n ) }
by A3, A4, Th14;
A7:
for x, y being set st x in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } & y in { (LSeg (f,l)) where l is Nat : ( m <= l & l < n ) } holds
x misses y
proof
let x,
y be
set ;
( x in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } & y in { (LSeg (f,l)) where l is Nat : ( m <= l & l < n ) } implies x misses y )
assume
x in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
;
( not y in { (LSeg (f,l)) where l is Nat : ( m <= l & l < n ) } or x misses y )
then consider k being
Nat such that A8:
x = LSeg (
f,
k)
and A9:
i <= k
and A10:
k < j
;
assume
y in { (LSeg (f,l)) where l is Nat : ( m <= l & l < n ) }
;
x misses y
then consider l being
Nat such that A11:
y = LSeg (
f,
l)
and A12:
m <= l
and A13:
l < n
;
A14:
l < len f
by A4, A13, XXREAL_0:2;
l + 1
<= n
by A13, NAT_1:13;
then A15:
(
k > 1 or
l + 1
< len f )
by A5, A9, XXREAL_0:2;
k + 1
<= j
by A10, NAT_1:13;
then
k + 1
< m
by A2, XXREAL_0:2;
then
k + 1
< l
by A12, XXREAL_0:2;
hence
x misses y
by A8, A11, A14, A15, GOBOARD5:def 4;
verum
end;
m <= len f
by A3, A4, XXREAL_0:2;
then
j < len f
by A2, XXREAL_0:2;
then
L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
by A1, Th14;
hence
L~ (mid (f,i,j)) misses L~ (mid (f,m,n))
by A6, A7, ZFMISC_1:126; verum