for X, Y being set st X c= Y holds
free_magma_carrier X c= free_magma_carrier Y