let R be comRing; :: thesis: for a, b being Element of R holds
( a divides b iff b in {a} -Ideal )
let a, b be Element of R; :: thesis: ( a divides b iff b in {a} -Ideal )
A: now :: thesis: ( a divides b implies b in {a} -Ideal )
assume a divides b ; :: thesis: b in {a} -Ideal
then consider c being Element of R such that
A1: a * c = b ;
b in { (a * r) where r is Element of R : verum } by A1;
hence b in {a} -Ideal by IDEAL_1:64; :: thesis: verum
end;
now :: thesis: ( b in {a} -Ideal implies a divides b )
assume b in {a} -Ideal ; :: thesis: a divides b
then b in { (a * r) where r is Element of R : verum } by IDEAL_1:64;
then consider c being Element of R such that
A1: a * c = b ;
thus a divides b by A1; :: thesis: verum
end;
hence ( a divides b iff b in {a} -Ideal ) by A; :: thesis: verum