let x be object ; :: according to GLPACY00:def 7 :: thesis: ( x in dom <*C*> implies ex G being _Graph st
( <*C*> . x = G & G is Cycle-like ) )
assume A1: x in dom <*C*> ; :: thesis: ex G being _Graph st
( <*C*> . x = G & G is Cycle-like )
then reconsider n = x as Nat ;
n in Seg 1 by A1, FINSEQ_1:def 8;
then n = 1 by TARSKI:def 1, FINSEQ_1:2;
hence ex G being _Graph st
( <*C*> . x = G & G is Cycle-like ) ; :: thesis: verum