theorem Lm1: :: ALGNUM_1:2

F_Rat is Subfield of F_Complex by EC_PF_1:5, GAUSSINT:14, RING_3:48;