let R be non empty doubleLoopStr ; :: thesis: for a, b being Element of R holds
( a in {a,b} -Ideal & b in {a,b} -Ideal )
let a, b be Element of R; :: thesis: ( a in {a,b} -Ideal & b in {a,b} -Ideal )
A1: {a} -Ideal c= {a,b} -Ideal by Lm2, Th57;
a in {a} -Ideal by Th66;
hence a in {a,b} -Ideal by A1; :: thesis: b in {a,b} -Ideal
A2: {b} -Ideal c= {a,b} -Ideal by Lm2, Th57;
b in {b} -Ideal by Th66;
hence b in {a,b} -Ideal by A2; :: thesis: verum