let C be _Graph; :: thesis: ( C is 3 -vertex & C is simple & C is complete implies C is Cycle-like )
assume A1: ( C is 3 -vertex & C is simple & C is complete ) ; :: thesis: C is Cycle-like
hence C is connected ; :: according to GLPACY00:def 6 :: thesis: ( not C is acyclic & C is 2 -regular )
C .order() = 3 by A1, GLIB_013:def 3;
hence not C is acyclic by A1, Th8; :: thesis: C is 2 -regular
C is 2 +` 1 -vertex by A1;
hence C is 2 -regular by A1; :: thesis: verum