reconsider y1 = y " as Real ;
assume ( x = a & y = b ) ; :: thesis: x / y = a / b
hence a / b = x * y1
.= x / y ;
:: thesis: verum