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