theorem :: GR_FREE0:15

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