theorem :: RING_3:103

for F being 0 -characteristic Field holds F includes F_Rat by Th71;