:: deftheorem Def6 defines complete CHORD:def 6 :
for G being _Graph holds
( G is complete iff for u, v being Vertex of G st u <> v holds
u,v are_adjacent );