per cases ( ( 1 <= i & i < len S ) or not 1 <= i or not i < len S ) ;
suppose A1: ( 1 <= i & i < len S ) ; :: thesis: ( not Segm (S,i) is empty & Segm (S,i) is compact )
then A2: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by Def4;
LE S /. i,S /. (i + 1),C by A1, Def3;
hence ( not Segm (S,i) is empty & Segm (S,i) is compact ) by A2, Th20, JORDAN7:6; :: thesis: verum
end;
suppose ( not 1 <= i or not i < len S ) ; :: thesis: ( not Segm (S,i) is empty & Segm (S,i) is compact )
then A3: Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) by Def4;
8 <= len S by Def3;
then 1 <= len S by XXREAL_0:2;
then A4: S /. (len S) in C by Th21;
S /. 1 = W-min C by Def3;
hence ( not Segm (S,i) is empty & Segm (S,i) is compact ) by A3, A4, Th19, JORDAN16:19; :: thesis: verum
end;
end;