let a, b, c be Integer; :: thesis: ( a * b divides c implies ( a divides c & b divides c ) )
( a divides a * b & b divides a * b ) ;
hence ( a * b divides c implies ( a divides c & b divides c ) ) by INT_2:9; :: thesis: verum