set j = the Element of I;
a * the Element of I in { (a * i) where i is Element of R : i in I } ;
hence not a * I is empty ; :: thesis: verum