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 6 :: 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:19;

hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A2, XXREAL_0:2; :: thesis: verum

assume A1: len f <= 2 ; :: thesis: f is unfolded

let i be Nat; :: according to TOPREAL1:def 6 :: 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:19;

hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A2, XXREAL_0:2; :: thesis: verum