reconsider c = 2 +` 1 as non empty Cardinal ;
take G = the simple complete c -vertex _Graph; :: thesis: ( not G is _trivial & G is Cycle-like )
G is 0 + 3 -vertex ;
hence ( not G is _trivial & G is Cycle-like ) ; :: thesis: verum