let
R
be
Ring
;
:: thesis:
R
is
RingExtension
of
R
R
is
Subring
of
R
by
Th1
;
hence
R
is
RingExtension
of
R
by
Def1
;
:: thesis:
verum