consider u being Element of R such that
A1: ( u divides x & u divides y ) and
A2: for zz being Element of R st zz divides x & zz divides y holds
zz divides u by Def11;
consider z being Element of Amp such that
A3: z is_associated_to u by Th22;
A4: for zz being Element of R st zz divides x & zz divides y holds
zz divides z
proof
let zz be Element of R; :: thesis: ( zz divides x & zz divides y implies zz divides z )
assume ( zz divides x & zz divides y ) ; :: thesis: zz divides z
then A5: zz divides u by A2;
u divides z by A3;
hence zz divides z by A5, Th2; :: thesis: verum
end;
z divides u by A3;
then ( z divides x & z divides y ) by A1, Th2;
hence ex b1 being Element of R st
( b1 in Amp & b1 divides x & b1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b1 ) ) by A4; :: thesis: verum