let i be Integer; :: thesis: i div 1 = i
thus i div 1 = [\(i / 1)/] by INT_1:def 9
.= i by INT_1:25 ; :: thesis: verum