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