theorem :: IDEAL_1:69

for R being non empty doubleLoopStr
for a, b being Element of R holds
( {a} -Ideal c= {a,b} -Ideal & {b} -Ideal c= {a,b} -Ideal ) by Lm2, Th57;