:: deftheorem Def8 defines Adjacent SCMYCIEL:def 8 :
for G being SimpleGraph
for v being Element of Vertices G
for b₃ being Subset of (Vertices G) holds
( b₃ = Adjacent v iff for x being Element of Vertices G holds
( x in b₃ iff {v,x} in Edges G ) );