reconsider E = F as FieldExtension of F by FIELD_4:6;
take E ; :: thesis: E is ordered
thus E is ordered ; :: thesis: verum