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