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 b1 being Ring st b1 is field-containing ; :: thesis: verum