let
R
be
domRing
;
:: thesis:
R
is
domRingExtension
of
R
R
is
Subring
of
R
by
Th1
;
hence
R
is
domRingExtension
of
R
by
Def1
;
:: thesis:
verum