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

len S >= 8 by Def3;

then len S >= 2 by XXREAL_0:2;

hence not S is trivial by NAT_D:60; :: thesis: verum