|.a.| in INT by INT_1:def 2;
hence |.a.| is Element of INT.Ring ; :: thesis: verum