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 ;
then ( H is strict Subgroup of G & not H is trivial ) by GROUP_2:def 5;
hence ex b₁ being Subgroup of G st
( b₁ is strict & not b₁ is trivial ) ; :: thesis: verum