let h be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being 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 Nat; :: thesis: ( 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 ; :: thesis: L~ (mid (h,i1,i2)) c= L~ h
thus L~ (mid (h,i1,i2)) c= L~ h :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ (mid (h,i1,i2)) or x in L~ h )
assume A5: x in L~ (mid (h,i1,i2)) ; :: thesis: x in L~ h

now :: thesis: ( ( i1 <= i2 & x in L~ h ) or ( i1 > i2 & x in L~ h ) )

per cases ( i1 <= i2 or i1 > i2 ) ;

case A6: i1 <= i2 ; :: thesis: x in L~ h

x in union { (LSeg ((mid (h,i1,i2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i1,i2)) ) } by A5, TOPREAL1:def 4;
then consider Y being set such that
A7: ( x in Y & Y in { (LSeg ((mid (h,i1,i2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i1,i2)) ) } ) by TARSKI:def 4;
consider i being 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 3;
len (mid (h,i1,i2)) = (i2 -' i1) + 1 by A1, A2, A3, A4, A6, FINSEQ_6:118;
then (i + 1) - 1 <= ((i2 -' i1) + 1) - 1 by A10, XREAL_1:9;
then i <= i2 - i1 by A6, XREAL_1:233;
then A12: i + i1 <= (i2 - i1) + i1 by XREAL_1:6;
then A13: i + i1 <= len h by A4, XXREAL_0:2;
1 + 1 <= i + i1 by A1, A9, XREAL_1:7;
then A14: (1 + 1) - 1 <= (i + i1) - 1 by XREAL_1:9;
then 1 <= (i + i1) -' 1 by A1, NAT_1:12, XREAL_1:233;
then A15: h /. ((i + i1) -' 1) = h . ((i + i1) -' 1) by A13, FINSEQ_4:15, 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, FINSEQ_6:118;
A17: ((i + 1) + i1) -' 1 = ((i + 1) + i1) - 1 by A1, NAT_1:12, XREAL_1:233
.= i + i1 ;
then A18: ((i + 1) + i1) -' 1 = ((i + i1) - 1) + 1
.= ((i + i1) -' 1) + 1 by A1, NAT_1:12, XREAL_1:233 ;
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:15;
A21: (mid (h,i1,i2)) /. (i + 1) = (mid (h,i1,i2)) . (i + 1) by A10, FINSEQ_4:15, 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, FINSEQ_6:118;
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:15, NAT_1:12
.= LSeg (h,((i + i1) -' 1)) by A14, A13, A17, A18, TOPREAL1:def 3 ;
then LSeg ((mid (h,i1,i2)),i) in { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) } by A14, A17, A18, A22;
then x in union { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) } by A7, A8, TARSKI:def 4;
hence x in L~ h by TOPREAL1:def 4; :: thesis: verum

end;

case A23: i1 > i2 ; :: thesis: 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 Nat : ( 1 <= i & i + 1 <= len (mid (h,i2,i1)) ) } by TOPREAL1:def 4;
then consider Y being set such that
A24: ( x in Y & Y in { (LSeg ((mid (h,i2,i1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i2,i1)) ) } ) by TARSKI:def 4;
consider i being 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 3;
len (mid (h,i2,i1)) = (i1 -' i2) + 1 by A1, A2, A3, A4, A23, FINSEQ_6:118;
then (i + 1) - 1 <= ((i1 -' i2) + 1) - 1 by A27, XREAL_1:9;
then i <= i1 - i2 by A23, XREAL_1:233;
then A29: i + i2 <= (i1 - i2) + i2 by XREAL_1:6;
then A30: i + i2 <= len h by A2, XXREAL_0:2;
1 + 1 <= i + i2 by A3, A26, XREAL_1:7;
then A31: (1 + 1) - 1 <= (i + i2) - 1 by XREAL_1:9;
then 1 <= (i + i2) -' 1 by A3, NAT_1:12, XREAL_1:233;
then A32: h /. ((i + i2) -' 1) = h . ((i + i2) -' 1) by A30, FINSEQ_4:15, 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, FINSEQ_6:118;
A34: ((i + 1) + i2) -' 1 = ((i + 1) + i2) - 1 by A3, NAT_1:12, XREAL_1:233
.= i + i2 ;
then A35: ((i + 1) + i2) -' 1 = ((i + i2) - 1) + 1
.= ((i + i2) -' 1) + 1 by A3, NAT_1:12, XREAL_1:233 ;
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:15;
A38: (mid (h,i2,i1)) /. (i + 1) = (mid (h,i2,i1)) . (i + 1) by A27, FINSEQ_4:15, 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, FINSEQ_6:118;
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:15, NAT_1:12
.= LSeg (h,((i + i2) -' 1)) by A31, A30, A34, A35, TOPREAL1:def 3 ;
then LSeg ((mid (h,i2,i1)),i) in { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) } by A31, A34, A35, A39;
then x in union { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) } by A24, A25, TARSKI:def 4;
hence x in L~ h by TOPREAL1:def 4; :: thesis: verum

end;

end;

end;

hence x in L~ h ; :: thesis: verum

end;