consider X being strict Ring;
set D = {X};
A1: for x being Element of {X} holds x is strict Ring by TARSKI:def 1;
take {X} ; :: thesis: ( {X} is Ring_DOMAIN-like & not {X} is empty )
thus ( {X} is Ring_DOMAIN-like & not {X} is empty ) by A1, Def12; :: thesis: verum