:: deftheorem Def9 defines SimpleGraph SCMYCIEL:def 9 :
for X being set
for b₂ being SimpleGraph holds
( b₂ is SimpleGraph of X iff Vertices b₂ = X );