:: deftheorem defines carrier/\ RING_3:def 9 :
for F being Field holds carrier/\ F = { x where x is Element of F : for K being Subfield of F holds x in K } ;