let i, j be natural Number ; :: thesis: ( i < j & i <> 0 implies not i / j is integer )
assume that
A1: i < j and
A2: i <> 0 ; :: thesis: not i / j is integer
assume i / j is integer ; :: thesis: contradiction
then reconsider r = i / j as Integer ;
r = [\r/] by INT_1:25
.= i div j by INT_1:def 9 ;
hence contradiction by A1, A2, Th27, XCMPLX_1:50; :: thesis: verum