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