for a being Element of G holds ((1). G) |^ a = (1). G by Th80;
then (1). G is normal by Def13;
hence ex b₁ being Subgroup of G st
( b₁ is strict & b₁ is normal ) ; :: thesis: verum