let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.n.c. implies Rev f is s.n.c. )

assume A1: f is s.n.c. ; :: thesis: Rev f is s.n.c.

let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((Rev f),i) misses LSeg ((Rev f),j) )

assume A2: i + 1 < j ; :: thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)

assume A1: f is s.n.c. ; :: thesis: Rev f is s.n.c.

let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((Rev f),i) misses LSeg ((Rev f),j) )

assume A2: i + 1 < j ; :: thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)

per cases
( i = 0 or j + 1 > len (Rev f) or ( i <> 0 & j + 1 <= len (Rev f) ) )
;

end;

suppose A3:
( i = 0 or j + 1 > len (Rev f) )
; :: thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)

hence LSeg ((Rev f),i) misses LSeg ((Rev f),j) ; :: thesis: verum

end;

now :: thesis: ( ( i = 0 & LSeg ((Rev f),i) = {} ) or ( j + 1 > len (Rev f) & LSeg ((Rev f),j) = {} ) )

then
(LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = {}
;end;

hence LSeg ((Rev f),i) misses LSeg ((Rev f),j) ; :: thesis: verum

suppose that
i <> 0
and

A4: j + 1 <= len (Rev f) ; :: thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)

A4: j + 1 <= len (Rev f) ; :: thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)

A5:
j <= j + 1
by NAT_1:11;

i <= i + 1 by NAT_1:11;

then A6: i < j by A2, XXREAL_0:2;

A7: len (Rev f) = len f by FINSEQ_5:def 3;

then reconsider j9 = (len f) - j as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;

j <= len f by A4, A7, A5, XXREAL_0:2;

then reconsider i9 = (len f) - i as Element of NAT by A6, INT_1:5, XXREAL_0:2;

A8: j9 + j = len f ;

(len f) - (i + 1) > j9 by A2, XREAL_1:10;

then (i9 - 1) + 1 > j9 + 1 by XREAL_1:6;

then A9: LSeg (f,i9) misses LSeg (f,j9) by A1;

i9 + i = len f ;

hence (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = (LSeg (f,i9)) /\ (LSeg ((Rev f),j)) by Th2

.= {} by A9, A8, Th2 ;

:: according to XBOOLE_0:def 7 :: thesis: verum

end;i <= i + 1 by NAT_1:11;

then A6: i < j by A2, XXREAL_0:2;

A7: len (Rev f) = len f by FINSEQ_5:def 3;

then reconsider j9 = (len f) - j as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;

j <= len f by A4, A7, A5, XXREAL_0:2;

then reconsider i9 = (len f) - i as Element of NAT by A6, INT_1:5, XXREAL_0:2;

A8: j9 + j = len f ;

(len f) - (i + 1) > j9 by A2, XREAL_1:10;

then (i9 - 1) + 1 > j9 + 1 by XREAL_1:6;

then A9: LSeg (f,i9) misses LSeg (f,j9) by A1;

i9 + i = len f ;

hence (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = (LSeg (f,i9)) /\ (LSeg ((Rev f),j)) by Th2

.= {} by A9, A8, Th2 ;

:: according to XBOOLE_0:def 7 :: thesis: verum