theorem :: RING_3:104

for F being 0 -characteristic Field
for E being Field st F includes E holds
E includes F_Rat