theorem :: RING_3:102

PrimeField F_Rat = F_Rat by GAUSSINT:26;