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 9 :: 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

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 5; :: thesis: verum

end;

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

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

end;

end;

end;

then (LSeg (Rev f),i) /\ (LSeg (Rev f),j) = {} ;
hence LSeg (Rev f),i misses LSeg (Rev f),j by XBOOLE_0:def 7; :: 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: len (Rev f) = len f by FINSEQ_5:def 3;
A6: j <= j + 1 by NAT_1:11;
then A7: j <= len f by A4, A5, XXREAL_0:2;
reconsider j' = (len f) - j as Element of NAT by A4, A5, A6, INT_1:18, XXREAL_0:2;
i <= i + 1 by NAT_1:11;
then i < j by A2, XXREAL_0:2;
then reconsider i' = (len f) - i as Element of NAT by A7, INT_1:18, XXREAL_0:2;
A8: j' + j = len f ;
(len f) - (i + 1) > j' by A2, XREAL_1:12;
then (i' - 1) + 1 > j' + 1 by XREAL_1:8;
then A9: LSeg f,i' misses LSeg f,j' by A1, TOPREAL1:def 9;
i' + i = len f ;
hence (LSeg (Rev f),i) /\ (LSeg (Rev f),j) = (LSeg f,i') /\ (LSeg (Rev f),j) by Th2
.= (LSeg f,i') /\ (LSeg f,j') by A8, Th2
.= {} by A9, XBOOLE_0:def 7 ;
:: according to XBOOLE_0:def 7 :: thesis: verum

end;

end;