:: deftheorem defines FreeAtoms GR_FREE0:def 1 :
for M0 being multMagma-yielding Function holds FreeAtoms M0 = *graph (Carrier M0);