let N be non empty MonoidalSubStr of G; :: thesis: N is commutative
N is SubStr of G by Th21;
hence N is commutative ; :: thesis: verum