let R be non empty add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; :: thesis: for a, b being Element of R holds {a,b} -Ideal = ({a} -Ideal) + ({b} -Ideal)
let a, b be Element of R; :: thesis: {a,b} -Ideal = ({a} -Ideal) + ({b} -Ideal)

A1: now :: thesis: for u being object st u in {a,b} -Ideal holds
u in ({a} -Ideal) + ({b} -Ideal)

let u be object ; :: thesis: ( u in {a,b} -Ideal implies u in ({a} -Ideal) + ({b} -Ideal) )
assume u in {a,b} -Ideal ; :: thesis: u in ({a} -Ideal) + ({b} -Ideal)
then u in { ((a * r) + (b * s)) where r, s is Element of R : verum } by Th65;
then consider r, s being Element of R such that
A2: u = (a * r) + (b * s) ;
b * s in { (b * v) where v is Element of R : verum } ;
then reconsider b9 = b * s as Element of {b} -Ideal by Th64;
a * r in { (a * v) where v is Element of R : verum } ;
then reconsider a9 = a * r as Element of {a} -Ideal by Th64;
a9 + b9 in { (x + y) where x, y is Element of R : ( x in {a} -Ideal & y in {b} -Ideal ) } ;
hence u in ({a} -Ideal) + ({b} -Ideal) by A2; :: thesis: verum

end;

now :: thesis: for u being object st u in ({a} -Ideal) + ({b} -Ideal) holds
u in {a,b} -Ideal

let u be object ; :: thesis: ( u in ({a} -Ideal) + ({b} -Ideal) implies u in {a,b} -Ideal )
assume u in ({a} -Ideal) + ({b} -Ideal) ; :: thesis: u in {a,b} -Ideal
then consider x, y being Element of R such that
A3: u = x + y and
A4: x in {a} -Ideal and
A5: y in {b} -Ideal ;
y in { (b * v) where v is Element of R : verum } by A5, Th64;
then A6: ex s being Element of R st y = b * s ;
x in { (a * v) where v is Element of R : verum } by A4, Th64;
then ex r being Element of R st x = a * r ;
then u in { ((a * v) + (b * d)) where v, d is Element of R : verum } by A3, A6;
hence u in {a,b} -Ideal by Th65; :: thesis: verum

end;

hence {a,b} -Ideal = ({a} -Ideal) + ({b} -Ideal) by A1, TARSKI:2; :: thesis: verum