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)

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

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

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

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

case i = 0 ; :: thesis: LSeg ((Rev f),i) = {}

hence LSeg ((Rev f),i) = {} by TOPREAL1:def 3; :: thesis: verum

end;

case j + 1 > len (Rev f) ; :: thesis: LSeg ((Rev f),j) = {}

hence LSeg ((Rev f),j) = {} by TOPREAL1:def 3; :: thesis: verum

end;

end;

end;

then (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = {} ;
hence LSeg ((Rev f),i) misses LSeg ((Rev f),j) ; :: thesis: verum

end;

suppose that i <> 0 and
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;

end;