set H = multMagma(# the carrier of G, the multF of G #);
reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ;
the multF of H = the multF of G || the carrier of H by RELSET_1:19;
then H is Subgroup of G by Def5;
hence ex b₁ being Subgroup of G st b₁ is strict ; :: thesis: verum