now :: thesis: for z1 being Element of R st z1 in Amp & z1 divides x & z1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z1 ) holds
for z2 being Element of R st z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) holds
z1 = z2

let z1 be Element of R; :: thesis: ( z1 in Amp & z1 divides x & z1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z1 ) implies for z2 being Element of R st z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) holds
z1 = z2 )
assume that
A6: z1 in Amp and
A7: ( z1 divides x & z1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z1 ) ) ; :: thesis: for z2 being Element of R st z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) holds
z1 = z2
let z2 be Element of R; :: thesis: ( z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) implies z1 = z2 )
assume that
A8: z2 in Amp and
A9: ( z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) ) ; :: thesis: z1 = z2
( z1 divides z2 & z2 divides z1 ) by A7, A9;
then z1 is_associated_to z2 ;
hence z1 = z2 by A6, A8, Th22; :: thesis: verum

end;

hence for b₁, b₂ being Element of R st b₁ in Amp & b₁ divides x & b₁ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₁ ) & b₂ in Amp & b₂ divides x & b₂ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₂ ) holds
b₁ = b₂ ; :: thesis: verum