theorem :: GR_FREE0:16

for M1, M2, M3 being non empty multMagma
for x3 being Element of M3 holds [3,x3] in FreeAtoms <*M1,M2,M3*>