ex R being Ring st R is field-containing

proof

set F = the Field;
take the Field ; :: thesis: the Field is field-containing
the Field is Subfield of the Field by FIELD_4:1;
then the Field is Subring of the Field by FIELD_5:12;
hence the Field is field-containing ; :: thesis: verum

end;

hence ex b₁ being Ring st b₁ is field-containing ; :: thesis: verum