theorem :: GAUSSINT:14

F_Rat is Subfield of F_Real by EC_PF_1:2, Th13;