let u, v be Integer; :: thesis: for p, q being Element of INT.Ring st u = p & v = q holds
( u divides v iff p divides q )
let p, q be Element of INT.Ring; :: thesis: ( u = p & v = q implies ( u divides v iff p divides q ) )
assume A1: ( u = p & v = q ) ; :: thesis: ( u divides v iff p divides q )

hereby :: thesis: ( p divides q implies u divides v )

assume u divides v ; :: thesis: p divides q
then consider w being Integer such that
A2: v = u * w ;
reconsider r = w as Element of INT.Ring by INT_1:def 2;
q = p * r by A1, A2;
hence p divides q by GCD_1:def 1; :: thesis: verum

end;

assume p divides q ; :: thesis: u divides v
then ex r being Element of INT.Ring st q = p * r by GCD_1:def 1;
hence u divides v by A1; :: thesis: verum