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 that
A1: f is s.n.c. and
A2: (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) c= {(f /. (1 + 1))} and
A3: (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 that
A4: 1 <= i and
A5: i + 2 <= len f ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
A6: 1 < i + 1 by A4, NAT_1:13;
then A7: LSeg (f,(i + 1)) = LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1))) by A5, TOPREAL1:def 3;
A8: 1 < (i + 1) + 1 by A6, NAT_1:13;
(i + 1) + 1 = i + 2 ;
then A9: i + 1 < len f by A5, NAT_1:13;
then A10: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def 3;
( f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) & f /. (i + 1) in LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1))) ) by RLTOPSP1:68;
then f /. (i + 1) in (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A10, A7, XBOOLE_0:def 4;
then A11: {(f /. (i + 1))} c= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by ZFMISC_1:31;
A12: i < len f by A9, NAT_1:13;

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 A2, A11; :: thesis: verum

end;

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

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

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

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

then ( (len f) - 2 = (len f) -' 2 & (len f) - 1 = (len f) -' 1 ) by A4, A6, NAT_D:39;
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A11, A14; :: thesis: verum

end;

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

1 < i by A4, A13, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A16: (1 + 1) - 1 <= i - 1 by XREAL_1:9;
i + 2 < len f by A5, A15, XXREAL_0:1;
then A17: ((i + 1) + 1) + 1 <= len f by NAT_1:13;

now :: thesis: not (LSeg (f,i)) /\ (LSeg (f,(i + 1))) <> {(f /. (i + 1))}

( f /. (i + 1) in LSeg (f,(i + 1)) & f /. (i + 1) in LSeg (f,i) ) by A10, A7, RLTOPSP1:68;
then f /. (i + 1) in (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by XBOOLE_0:def 4;
then A18: {(f /. (i + 1))} c= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by ZFMISC_1:31;
assume (LSeg (f,i)) /\ (LSeg (f,(i + 1))) <> {(f /. (i + 1))} ; :: thesis: contradiction
then not (LSeg (f,i)) /\ (LSeg (f,(i + 1))) c= {(f /. (i + 1))} by A18;
then consider x being object such that
A19: x in (LSeg (f,i)) /\ (LSeg (f,(i + 1))) and
A20: not x in {(f /. (i + 1))} ;
A21: LSeg (f,((i + 1) + 1)) = LSeg ((f /. ((i + 1) + 1)),(f /. (((i + 1) + 1) + 1))) by A8, A17, TOPREAL1:def 3;
A22: x <> f /. (i + 1) by A20, TARSKI:def 1;

now :: thesis: ( ( f /. i in LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1))) & contradiction ) or ( f /. ((i + 1) + 1) in LSeg ((f /. i),(f /. (i + 1))) & contradiction ) )

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 A10, A7, A19, A22, Th16;

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

A24: i -' 1 = i - 1 by A4, XREAL_1:233;
then (i -' 1) + 1 < i + 1 by NAT_1:13;
then LSeg (f,(i -' 1)) misses LSeg (f,(i + 1)) by A1, TOPREAL1:def 7;
then A25: (LSeg (f,(i -' 1))) /\ (LSeg (f,(i + 1))) = {} ;
LSeg (f,(i -' 1)) = LSeg ((f /. (i -' 1)),(f /. ((i -' 1) + 1))) by A12, A16, A24, TOPREAL1:def 3;
then f /. i in LSeg (f,(i -' 1)) by A24, RLTOPSP1:68;
hence contradiction by A7, A23, A25, XBOOLE_0:def 4; :: thesis: verum

end;

case A26: 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 7;
then A27: (LSeg (f,i)) /\ (LSeg (f,((i + 1) + 1))) = {} ;
f /. ((i + 1) + 1) in LSeg (f,((i + 1) + 1)) by A21, RLTOPSP1:68;
hence contradiction by A10, A26, A27, 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 6; :: thesis: verum