let f, g be FinSequence of (TOP-REAL 2); ( g is_in_the_area_of f implies Rev g is_in_the_area_of f )
assume A1:
g is_in_the_area_of f
; Rev g is_in_the_area_of f
A2:
Rev (Rev g) = g
;
let n be Nat; SPRECT_2:def 1 ( not n in dom (Rev g) or ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) ) )
assume A3:
n in dom (Rev g)
; ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) )
n >= 1
by A3, FINSEQ_3:25;
then A4:
n - 1 >= 0
by XREAL_1:48;
set i = ((len g) + 1) -' n;
A5:
len (Rev g) = len g
by FINSEQ_5:def 3;
then A6:
n <= len g
by A3, FINSEQ_3:25;
then A7:
((len g) + 1) -' n = ((len g) -' n) + 1
by NAT_D:38;
then ((len g) + 1) -' n =
((len g) - n) + 1
by A6, XREAL_1:233
.=
(len g) - (n - 1)
;
then A8:
((len g) + 1) -' n <= (len g) - 0
by A4, XREAL_1:13;
1 <= ((len g) + 1) -' n
by A7, NAT_1:11;
then A9:
((len g) + 1) -' n in dom g
by A8, FINSEQ_3:25;
len g <= (len g) + 1
by NAT_1:11;
then
n + (((len g) + 1) -' n) = (len g) + 1
by A6, XREAL_1:235, XXREAL_0:2;
then
(Rev g) /. n = g /. (((len g) + 1) -' n)
by A2, A5, A3, FINSEQ_5:66;
hence
( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) )
by A1, A9; verum