let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f <= 2 implies f is unfolded )
assume A1: len f <= 2 ; :: thesis: f is unfolded
let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} )
assume A2: 1 <= i ; :: thesis: ( not i + 2 <= len f or (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} )
assume i + 2 <= len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}
then i + 2 <= 2 by A1, XXREAL_0:2;
then i <= 2 - 2 by XREAL_1:21;
hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A2, XXREAL_0:2; :: thesis: verum