theorem Th9: :: GR_FREE0:8

for x being object
for I being non empty set
for i being Element of I
for N being multMagma-Family of I holds
( [i,x] in FreeAtoms N iff x in the carrier of (N . i) )