let f be FinSequence of (TOP-REAL 2); ( len f <= 2 implies f is unfolded )
assume A1:
len f <= 2
; f is unfolded
let i be Nat; TOPREAL1:def 6 ( not 1 <= i or not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
assume A2:
1 <= i
; ( not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
assume
i + 2 <= len f
; (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; verum