:: deftheorem Def16 defines graph COHSP_1:def 16 :
for f being Function
for b₂ being set holds
( b₂ = graph f iff for x being set holds
( x in b₂ iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) );