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