theorem Th23: :: ALGSTR_4:23

for X, Y being set
for n being Nat st X c= Y holds
free_magma (X,n) c= free_magma (Y,n)