for x, y being Element of F_Rat
for x1, y1 being Rational st x1 = x & y1 = y & y <> 0. F_Rat holds
x / y = x1 / y1 by Th15;