theorem Th7: :: FIELD_3:7

for F being non almost_trivial Field
for x being non trivial Element of F
for o being object st not o in [#] F holds
( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )