:: deftheorem defines .set GLIB_000:def 12 :
for G being GraphStruct
for n being Nat
for x being set holds G .set (n,x) = G +* (n .--> x);