set m = the Element of M;
the Element of M is strict RingMorphism by Def12;
hence ex b₁ being Element of M st b₁ is strict ; :: thesis: verum