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

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

end;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 ) )end;

hence
x in L~ h
; :: thesis: verumper cases
( i1 <= i2 or i1 > i2 )
;

end;

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;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

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;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