b - [\b/] = b ;
hence frac b = b by INT_1:def 8; :: thesis: verum