consider m being Element of M;
m is strict RingMorphism by Def13;
hence ex b₁ being Element of M st b₁ is strict ; :: thesis: verum