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

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