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 )
( {a} -Ideal c= {a,b} -Ideal & a in {a} -Ideal ) by Lm2, Th57, Th66;
hence a in {a,b} -Ideal ; :: thesis: b in {a,b} -Ideal
( {b} -Ideal c= {a,b} -Ideal & b in {b} -Ideal ) by Lm2, Th57, Th66;
hence b in {a,b} -Ideal ; :: thesis: verum