T . i is Element of divs A ;
hence T . i is Division of A by INTEGRA1:def 3; :: thesis: verum