let a, b be Element of Gauss_INT_Ring; :: thesis: for aa, bb being G_INTEG st a = aa & b = bb & a divides b holds
aa Divides bb
let aa, bb be G_INTEG; :: thesis: ( a = aa & b = bb & a divides b implies aa Divides bb )
assume A1: ( a = aa & b = bb ) ; :: thesis: ( not a divides b or aa Divides bb )
assume a divides b ; :: thesis: aa Divides bb
then consider c being Element of Gauss_INT_Ring such that
A2: b = a * c by GCD_1:def 1;
reconsider cc = c as G_INTEG by Th2;
bb = aa * cc by A1, A2, Th6;
hence aa Divides bb ; :: thesis: verum