let x be _Graph; :: according to GLPACY00:def 10 :: thesis: ( x in {C1,C2} implies x is Cycle-like )
assume x in {C1,C2} ; :: thesis: x is Cycle-like

per cases then ( x = C1 or x = C2 ) by TARSKI:def 2;

suppose x = C1 ; :: thesis: x is Cycle-like

hence x is Cycle-like ; :: thesis: verum

end;

suppose x = C2 ; :: thesis: x is Cycle-like

hence x is Cycle-like ; :: thesis: verum

end;

end;