let h be FinSequence of (TOP-REAL 2); for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds
L~ (mid h,i1,i2) c= L~ h
let i1, i2 be Element of NAT ; ( 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h implies L~ (mid h,i1,i2) c= L~ h )
assume that
A1:
1 <= i1
and
A2:
i1 <= len h
and
A3:
1 <= i2
and
A4:
i2 <= len h
; L~ (mid h,i1,i2) c= L~ h
thus
L~ (mid h,i1,i2) c= L~ h
verumproof
let x be
set ;
TARSKI:def 3 ( not x in L~ (mid h,i1,i2) or x in L~ h )
assume A5:
x in L~ (mid h,i1,i2)
;
x in L~ h
now per cases
( i1 <= i2 or i1 > i2 )
;
case A6:
i1 <= i2
;
x in L~ h
x in union { (LSeg (mid h,i1,i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i1,i2) ) }
by A5, TOPREAL1:def 6;
then consider Y being
set such that A7:
(
x in Y &
Y in { (LSeg (mid h,i1,i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i1,i2) ) } )
by TARSKI:def 4;
consider i being
Element of
NAT such that A8:
Y = LSeg (mid h,i1,i2),
i
and A9:
1
<= i
and A10:
i + 1
<= len (mid h,i1,i2)
by A7;
A11:
LSeg (mid h,i1,i2),
i = LSeg ((mid h,i1,i2) /. i),
((mid h,i1,i2) /. (i + 1))
by A9, A10, TOPREAL1:def 5;
len (mid h,i1,i2) = (i2 -' i1) + 1
by A1, A2, A3, A4, A6, Th27;
then
(i + 1) - 1
<= ((i2 -' i1) + 1) - 1
by A10, XREAL_1:11;
then
i <= i2 - i1
by A6, XREAL_1:235;
then A12:
i + i1 <= (i2 - i1) + i1
by XREAL_1:8;
then A13:
i + i1 <= len h
by A4, XXREAL_0:2;
1
+ 1
<= i + i1
by A1, A9, XREAL_1:9;
then A14:
(1 + 1) - 1
<= (i + i1) - 1
by XREAL_1:11;
then
1
<= (i + i1) -' 1
by A1, NAT_1:12, XREAL_1:235;
then A15:
h /. ((i + i1) -' 1) = h . ((i + i1) -' 1)
by A13, FINSEQ_4:24, NAT_D:44;
1
<= i + 1
by NAT_1:11;
then A16:
(mid h,i1,i2) . (i + 1) = h . (((i + 1) + i1) -' 1)
by A1, A2, A3, A4, A6, A10, Th27;
A17:
((i + 1) + i1) -' 1 =
((i + 1) + i1) - 1
by A1, NAT_1:12, XREAL_1:235
.=
i + i1
;
then A18:
((i + 1) + i1) -' 1 =
((i + i1) - 1) + 1
.=
((i + i1) -' 1) + 1
by A1, NAT_1:12, XREAL_1:235
;
i <= i + 1
by NAT_1:11;
then A19:
i <= len (mid h,i1,i2)
by A10, XXREAL_0:2;
then A20:
(mid h,i1,i2) /. i = (mid h,i1,i2) . i
by A9, FINSEQ_4:24;
A21:
(mid h,i1,i2) /. (i + 1) = (mid h,i1,i2) . (i + 1)
by A10, FINSEQ_4:24, NAT_1:11;
A22:
i + i1 <= len h
by A4, A12, XXREAL_0:2;
(mid h,i1,i2) . i = h . ((i + i1) -' 1)
by A1, A2, A3, A4, A6, A9, A19, Th27;
then LSeg (mid h,i1,i2),
i =
LSeg (h /. ((i + i1) -' 1)),
(h /. (((i + 1) + i1) -' 1))
by A1, A11, A16, A20, A21, A15, A17, A22, FINSEQ_4:24, NAT_1:12
.=
LSeg h,
((i + i1) -' 1)
by A14, A13, A17, A18, TOPREAL1:def 5
;
then
LSeg (mid h,i1,i2),
i in { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A14, A17, A18, A22;
then
x in union { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A7, A8, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 6;
verum end; case A23:
i1 > i2
;
x in L~ h
mid h,
i1,
i2 = Rev (mid h,i2,i1)
by Lm6;
then
x in L~ (mid h,i2,i1)
by A5, SPPOL_2:22;
then
x in union { (LSeg (mid h,i2,i1),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i2,i1) ) }
by TOPREAL1:def 6;
then consider Y being
set such that A24:
(
x in Y &
Y in { (LSeg (mid h,i2,i1),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i2,i1) ) } )
by TARSKI:def 4;
consider i being
Element of
NAT such that A25:
Y = LSeg (mid h,i2,i1),
i
and A26:
1
<= i
and A27:
i + 1
<= len (mid h,i2,i1)
by A24;
A28:
LSeg (mid h,i2,i1),
i = LSeg ((mid h,i2,i1) /. i),
((mid h,i2,i1) /. (i + 1))
by A26, A27, TOPREAL1:def 5;
len (mid h,i2,i1) = (i1 -' i2) + 1
by A1, A2, A3, A4, A23, Th27;
then
(i + 1) - 1
<= ((i1 -' i2) + 1) - 1
by A27, XREAL_1:11;
then
i <= i1 - i2
by A23, XREAL_1:235;
then A29:
i + i2 <= (i1 - i2) + i2
by XREAL_1:8;
then A30:
i + i2 <= len h
by A2, XXREAL_0:2;
1
+ 1
<= i + i2
by A3, A26, XREAL_1:9;
then A31:
(1 + 1) - 1
<= (i + i2) - 1
by XREAL_1:11;
then
1
<= (i + i2) -' 1
by A3, NAT_1:12, XREAL_1:235;
then A32:
h /. ((i + i2) -' 1) = h . ((i + i2) -' 1)
by A30, FINSEQ_4:24, NAT_D:44;
1
<= i + 1
by NAT_1:11;
then A33:
(mid h,i2,i1) . (i + 1) = h . (((i + 1) + i2) -' 1)
by A1, A2, A3, A4, A23, A27, Th27;
A34:
((i + 1) + i2) -' 1 =
((i + 1) + i2) - 1
by A3, NAT_1:12, XREAL_1:235
.=
i + i2
;
then A35:
((i + 1) + i2) -' 1 =
((i + i2) - 1) + 1
.=
((i + i2) -' 1) + 1
by A3, NAT_1:12, XREAL_1:235
;
i <= i + 1
by NAT_1:11;
then A36:
i <= len (mid h,i2,i1)
by A27, XXREAL_0:2;
then A37:
(mid h,i2,i1) /. i = (mid h,i2,i1) . i
by A26, FINSEQ_4:24;
A38:
(mid h,i2,i1) /. (i + 1) = (mid h,i2,i1) . (i + 1)
by A27, FINSEQ_4:24, NAT_1:11;
A39:
i + i2 <= len h
by A2, A29, XXREAL_0:2;
(mid h,i2,i1) . i = h . ((i + i2) -' 1)
by A1, A2, A3, A4, A23, A26, A36, Th27;
then LSeg (mid h,i2,i1),
i =
LSeg (h /. ((i + i2) -' 1)),
(h /. (((i + 1) + i2) -' 1))
by A3, A28, A33, A37, A38, A32, A34, A39, FINSEQ_4:24, NAT_1:12
.=
LSeg h,
((i + i2) -' 1)
by A31, A30, A34, A35, TOPREAL1:def 5
;
then
LSeg (mid h,i2,i1),
i in { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A31, A34, A35, A39;
then
x in union { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A24, A25, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 6;
verum end;
hence
x in L~ h
;
verum
end;