a . i in Ideals A ;
then a . i in { I where I is Ideal of A : verum } by RING_2:def 3;
then consider ai being Ideal of A such that
A2: ai = a . i ;
thus a . i is non empty Subset of A by A2; :: thesis: verum