:: deftheorem Def9 defines simple GRAPH_1:def 9 :
for IT being Graph holds
( IT is simple iff for x being set holds
( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x ) );