let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.n.c. & (LSeg f,1) /\ (LSeg f,(1 + 1)) c= {(f /. (1 + 1))} & (LSeg f,((len f) -' 2)) /\ (LSeg f,((len f) -' 1)) c= {(f /. ((len f) -' 1))} implies f is unfolded )
assume A1: ( f is s.n.c. & (LSeg f,1) /\ (LSeg f,(1 + 1)) c= {(f /. (1 + 1))} & (LSeg f,((len f) -' 2)) /\ (LSeg f,((len f) -' 1)) c= {(f /. ((len f) -' 1))} ) ; :: thesis: f is unfolded
for i being Nat st 1 <= i & i + 2 <= len f holds
(LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

proof

let i be Nat; :: thesis: ( 1 <= i & i + 2 <= len f implies (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} )
assume A2: ( 1 <= i & i + 2 <= len f ) ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}
A3: (i + 1) + 1 = i + 2 ;
A4: 1 < i + 1 by A2, NAT_1:13;
A5: i + 1 < len f by A2, A3, NAT_1:13;
then A6: i < len f by NAT_1:13;
A7: 1 < (i + 1) + 1 by A4, NAT_1:13;
A8: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, A5, TOPREAL1:def 5;
A9: LSeg f,(i + 1) = LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) by A2, A4, TOPREAL1:def 5;
A10: f /. (i + 1) in LSeg (f /. i),(f /. (i + 1)) by RLTOPSP1:69;
f /. (i + 1) in LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) by RLTOPSP1:69;
then f /. (i + 1) in (LSeg f,i) /\ (LSeg f,(i + 1)) by A8, A9, A10, XBOOLE_0:def 4;
then A11: {(f /. (i + 1))} c= (LSeg f,i) /\ (LSeg f,(i + 1)) by ZFMISC_1:37;

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A1, A11, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A12: i <> 1 ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

now

per cases ( i + 2 = len f or i + 2 <> len f ) ;

case A13: i + 2 = len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

then A14: (len f) - 2 = (len f) -' 2 by A2, NAT_D:39;
(len f) - 1 = (len f) -' 1 by A4, A13, NAT_D:39;
hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A1, A11, A13, A14, XBOOLE_0:def 10; :: thesis: verum

end;

case i + 2 <> len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

then i + 2 < len f by A2, XXREAL_0:1;
then A15: ((i + 1) + 1) + 1 <= len f by NAT_1:13;
1 < i by A2, A12, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A16: (1 + 1) - 1 <= i - 1 by XREAL_1:11;

now

assume A17: (LSeg f,i) /\ (LSeg f,(i + 1)) <> {(f /. (i + 1))} ; :: thesis: contradiction
A18: f /. (i + 1) in LSeg f,(i + 1) by A9, RLTOPSP1:69;
f /. (i + 1) in LSeg f,i by A8, RLTOPSP1:69;
then f /. (i + 1) in (LSeg f,i) /\ (LSeg f,(i + 1)) by A18, XBOOLE_0:def 4;
then {(f /. (i + 1))} c= (LSeg f,i) /\ (LSeg f,(i + 1)) by ZFMISC_1:37;
then not (LSeg f,i) /\ (LSeg f,(i + 1)) c= {(f /. (i + 1))} by A17, XBOOLE_0:def 10;
then consider x being set such that
A19: ( x in (LSeg f,i) /\ (LSeg f,(i + 1)) & not x in {(f /. (i + 1))} ) by TARSKI:def 3;
A20: x <> f /. (i + 1) by A19, TARSKI:def 1;
A21: LSeg f,((i + 1) + 1) = LSeg (f /. ((i + 1) + 1)),(f /. (((i + 1) + 1) + 1)) by A7, A15, TOPREAL1:def 5;

now

per cases ( f /. i in LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) or f /. ((i + 1) + 1) in LSeg (f /. i),(f /. (i + 1)) ) by A8, A9, A19, A20, Th20;

case A22: f /. i in LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) ; :: thesis: contradiction

A23: i -' 1 = i - 1 by A2, XREAL_1:235;
then (i -' 1) + 1 < i + 1 by NAT_1:13;
then LSeg f,(i -' 1) misses LSeg f,(i + 1) by A1, TOPREAL1:def 9;
then A24: (LSeg f,(i -' 1)) /\ (LSeg f,(i + 1)) = {} by XBOOLE_0:def 7;
LSeg f,(i -' 1) = LSeg (f /. (i -' 1)),(f /. ((i -' 1) + 1)) by A6, A16, A23, TOPREAL1:def 5;
then f /. i in LSeg f,(i -' 1) by A23, RLTOPSP1:69;
hence contradiction by A9, A22, A24, XBOOLE_0:def 4; :: thesis: verum

end;

case A25: f /. ((i + 1) + 1) in LSeg (f /. i),(f /. (i + 1)) ; :: thesis: contradiction

i + 1 < (i + 1) + 1 by NAT_1:13;
then LSeg f,i misses LSeg f,((i + 1) + 1) by A1, TOPREAL1:def 9;
then A26: (LSeg f,i) /\ (LSeg f,((i + 1) + 1)) = {} by XBOOLE_0:def 7;
f /. ((i + 1) + 1) in LSeg f,((i + 1) + 1) by A21, RLTOPSP1:69;
hence contradiction by A8, A25, A26, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

hence f is unfolded by TOPREAL1:def 8; :: thesis: verum