theorem :: XREAL_1:225

for a, b being Real st b <> 0 holds
ex c being Real st a = b / c