let S be Segmentation of C; :: thesis: not S is trivial
len S >= 8 by Def3;
then len S >= 2 by XXREAL_0:2;
hence not S is trivial by NAT_D:60; :: thesis: verum