let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: Rev g is_in_the_area_of f
A2: Rev (Rev g) = g by FINSEQ_6:29;
A3: len (Rev g) = len g by FINSEQ_5:def 3;
let n be Element of NAT ; :: according to SPRECT_2:def 1 :: thesis: ( 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 A4: n in dom (Rev g) ; :: thesis: ( 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) )
set i = ((len g) + 1) -' n;
A5: n <= len g by A3, A4, FINSEQ_3:27;
len g <= (len g) + 1 by NAT_1:11;
then n + (((len g) + 1) -' n) = (len g) + 1 by A5, XREAL_1:237, XXREAL_0:2;
then A6: (Rev g) /. n = g /. (((len g) + 1) -' n) by A2, A3, A4, FINSEQ_5:69;
A7: ((len g) + 1) -' n = ((len g) -' n) + 1 by A5, NAT_D:38;
then A8: 1 <= ((len g) + 1) -' n by NAT_1:11;
A9: ((len g) + 1) -' n = ((len g) - n) + 1 by A5, A7, XREAL_1:235
.= (len g) - (n - 1) ;
n >= 1 by A4, FINSEQ_3:27;
then n - 1 >= 0 by XREAL_1:50;
then ((len g) + 1) -' n <= (len g) - 0 by A9, XREAL_1:15;
then ((len g) + 1) -' n in dom g by A8, FINSEQ_3:27;
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, A6, SPRECT_2:def 1; :: thesis: verum