theorem :: GR_FREE0:14

for M1, M2, M3 being non empty multMagma
for x1 being Element of M1 holds
( [1,x1] in FreeAtoms <*M1*> & [1,x1] in FreeAtoms <*M1,M2*> & [1,x1] in FreeAtoms <*M1,M2,M3*> )