consider G being Ring;
take {(ID G)} ; :: thesis: {(ID G)} is RingMorphism_DOMAIN-like
for x being set st x in {(ID G)} holds
x is strict RingMorphism by TARSKI:def 1;
hence {(ID G)} is RingMorphism_DOMAIN-like by Def13; :: thesis: verum