theorem Lm48: :: ALGNUM_1:39

for x being Element of F_Complex
for a being Element of F_Rat holds a in FQ x