dom a <> {} by RELAT_1:41;
then a . i in rng a by FUNCT_1:3;
then 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 for b₁ being Subset of A st b₁ = a . i holds
( b₁ is add-closed & b₁ is left-ideal & b₁ is right-ideal ) by A2; :: thesis: verum