let x, y be Integer; :: thesis: for a, b being Element of INT.Ring st x <> 0 & x = a & y = b holds
( x divides y iff a divides b )
let a, b be Element of INT.Ring; :: thesis: ( x <> 0 & x = a & y = b implies ( x divides y iff a divides b ) )
assume AS: ( x <> 0 & x = a & y = b ) ; :: thesis: ( x divides y iff a divides b )

now :: thesis: ( x divides y implies a divides b )

assume x divides y ; :: thesis: a divides b
then consider z being Integer such that
H: x * z = y by INT_1:def 3;
reconsider c = z as Element of INT.Ring by INT_1:def 2, INT_3:def 3;
a * c = b by H, AS;
hence a divides b ; :: thesis: verum

end;

hence ( x divides y iff a divides b ) by AS, INT_1:def 3; :: thesis: verum