theorem Th15: :: GAUSSINT:15

for x being Element of F_Rat
for x1 being Rational st x <> 0. F_Rat & x1 = x holds
x " = x1 "