consider F being strict Field;
reconsider F = F as Ring ;
F is comRing ;
hence ex b₁ being comRing st b₁ is strict ; :: thesis: verum