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 & not b₁ is empty ) ; :: thesis: verum