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 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: 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:18, 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:18, XXREAL_0:2;
A8: j9 + j = len f ;
(len f) - (i + 1) > j9 by A2, XREAL_1:12;
then (i9 - 1) + 1 > j9 + 1 by XREAL_1:8;
then A9: LSeg f,i9 misses LSeg f,j9 by A1, TOPREAL1:def 9;
i9 + i = len f ;
hence (LSeg (Rev f),i) /\ (LSeg (Rev f),j) = (LSeg f,i9) /\ (LSeg (Rev f),j) by Th2
.= (LSeg f,i9) /\ (LSeg f,j9) by A8, Th2
.= {} by A9, XBOOLE_0:def 7 ;
:: according to XBOOLE_0:def 7 :: thesis: verum
end;
end;