let R be non empty add-cancelable Abelian add-associative right_zeroed associative commutative well-unital distributive 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

let u be set ; :: 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) ;
a * r in { (a * v) where v is Element of R : verum } ;
then reconsider a' = a * r as Element of {a} -Ideal by Th64;
b * s in { (b * v) where v is Element of R : verum } ;
then reconsider b' = b * s as Element of {b} -Ideal by Th64;
a' + b' 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

let u be set ; :: 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 & x in {a} -Ideal & y in {b} -Ideal ) ;
x in { (a * v) where v is Element of R : verum } by A3, Th64;
then consider r being Element of R such that
A4: x = a * r ;
y in { (b * v) where v is Element of R : verum } by A3, Th64;
then consider s being Element of R such that
A5: y = b * s ;
u in { ((a * v) + (b * d)) where v, d is Element of R : verum } by A3, A4, A5;
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