take nabla the carrier of M ; :: thesis: nabla the carrier of M is compatible
thus nabla the carrier of M is compatible ; :: thesis: verum