let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f <= 2 implies f is s.n.c. )
assume A1: len f <= 2 ; :: thesis: f is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) )
assume A2: i + 1 < j ; :: thesis: LSeg (f,i) misses LSeg (f,j)
now :: thesis: ( 1 <= i & i + 1 <= len f & 1 <= j implies not j + 1 <= len f )
assume that
A3: 1 <= i and
A4: i + 1 <= len f and
A5: 1 <= j and
A6: j + 1 <= len f ; :: thesis: contradiction
j + 1 <= 1 + 1 by A1, A6, XXREAL_0:2;
then j <= 1 by XREAL_1:6;
then A7: j = 1 by A5, XXREAL_0:1;
i + 1 <= 1 + 1 by A1, A4, XXREAL_0:2;
then i <= 1 by XREAL_1:6;
then i = 1 by A3, XXREAL_0:1;
hence contradiction by A2, A7; :: thesis: verum
end;
then ( LSeg (f,i) = {} or LSeg (f,j) = {} ) by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum