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

assume that
A3: 1 <= i and
A4: i + 1 <= len f and
A5: 1 <= j and
A6: j + 1 <= len f ; :: thesis: contradiction
( i + 1 <= 1 + 1 & j + 1 <= 1 + 1 ) by A1, A4, A6, XXREAL_0:2;
then ( i <= 1 & j <= 1 ) by XREAL_1:8;
then ( i = 1 & j = 1 ) by A3, A5, XXREAL_0:1;
hence contradiction by A2; :: thesis: verum

end;

then ( LSeg f,i = {} or LSeg f,j = {} ) by TOPREAL1:def 5;
hence (LSeg f,i) /\ (LSeg f,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum