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