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