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)

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

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 )

then
( LSeg (f,i) = {} or LSeg (f,j) = {} )
by TOPREAL1:def 3;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;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

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