theorem lift5a: :: FIELD_12:34

for F being Field
for E being FieldExtension of F holds id F is Monomorphism of F,E