multMagma(# the carrier of G, the multF of G #) is SubStr of G by Def23;
hence ex b₁ being SubStr of G st b₁ is strict ; :: thesis: verum