INT.Group is cyclic by Def9, Lm5;
hence ex b₁ being Group st
( b₁ is strict & b₁ is cyclic ) ; :: thesis: verum