let
i
be
Integer
;
:: thesis:
i
in
the
carrier
of
INT.Ring
i
in
INT
by
INT_1:def 2
;
hence
i
in
the
carrier
of
INT.Ring
;
:: thesis:
verum