theorem :: ALGSTR_4:28

for X being set
for n being Nat st n > 0 holds
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X by Lm1;