theorem :: ALGNUM_1:48

for x being Element of F_Complex holds F_Rat is Subring of FQ_Ring x