let a, b be Integer; :: thesis: ( a divides b implies b / a is integer )
not ( not a = 0 & a divides b & not b / a is integer ) by WSIERP_1:17;
hence ( a divides b implies b / a is integer ) ; :: thesis: verum