consider z being Element of L such that
H: ( z divides x & z divides y & ( for zz being Element of L st zz divides x & zz divides y holds
zz divides z ) ) by GCD_1:def 11;
take z ; :: thesis: z is x,y -gcd
thus z is x,y -gcd by H; :: thesis: verum