let R be EuclidianRing; :: thesis: for a, b being Element of R
for g being a_gcd of a,b holds {g} -Ideal = {a,b} -Ideal
let a, b be Element of R; :: thesis: for g being a_gcd of a,b holds {g} -Ideal = {a,b} -Ideal
let g be a_gcd of a,b; :: thesis: {g} -Ideal = {a,b} -Ideal
HX: ( {a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum } & {g} -Ideal = { (g * r) where r is Element of R : verum } ) by IDEAL_1:64, IDEAL_1:65;
consider r, s being Element of R such that
H1: g = (a * r) + (b * s) by lemgcdii;
H2: g in {a,b} -Ideal by H1, HX;

now :: thesis: for o being object st o in {a,b} -Ideal holds
o in {g} -Ideal

let o be object ; :: thesis: ( o in {a,b} -Ideal implies o in {g} -Ideal )
assume o in {a,b} -Ideal ; :: thesis: o in {g} -Ideal
then consider r, s being Element of R such that
H1: o = (a * r) + (b * s) by HX;
g divides a by RING_4:def 10;
then consider c being Element of R such that
H2: a = g * c by GCD_1:def 1;
g divides b by RING_4:def 10;
then consider e being Element of R such that
H3: b = g * e by GCD_1:def 1;
o = (g * (c * r)) + ((g * e) * s) by H1, H2, H3, GROUP_1:def 3
.= (g * (c * r)) + (g * (e * s)) by GROUP_1:def 3
.= g * ((c * r) + (e * s)) by VECTSP_1:def 2 ;
hence o in {g} -Ideal by HX; :: thesis: verum

end;

then {a,b} -Ideal c= {g} -Ideal ;
hence {g} -Ideal = {a,b} -Ideal by H2, IDEAL_1:67; :: thesis: verum