set F = the non almost_trivial Field;

set x = the non trivial Element of the non almost_trivial Field;

reconsider o = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> as object ;

set x = the non trivial Element of the non almost_trivial Field;

reconsider o = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> as object ;

per cases
( not o in [#] the non almost_trivial Field or ex a being Element of the non almost_trivial Field st a = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> )
;

end;

suppose
not o in [#] the non almost_trivial Field
; :: thesis: ex K being Field st ([#] K) /\ ([#] (Polynom-Ring K)) <> {}

then reconsider K = ExField ( the non trivial Element of the non almost_trivial Field,o) as Field by Th7, Th8, Th10, Th9, Th12, Th11;

take K ; :: thesis: ([#] K) /\ ([#] (Polynom-Ring K)) <> {}

thus ([#] K) /\ ([#] (Polynom-Ring K)) <> {} by Th13; :: thesis: verum

end;take K ; :: thesis: ([#] K) /\ ([#] (Polynom-Ring K)) <> {}

thus ([#] K) /\ ([#] (Polynom-Ring K)) <> {} by Th13; :: thesis: verum

suppose A1:
ex a being Element of the non almost_trivial Field st a = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%>
; :: thesis: ex K being Field st ([#] K) /\ ([#] (Polynom-Ring K)) <> {}

take
the non almost_trivial Field
; :: thesis: ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) <> {}

<%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> in [#] (Polynom-Ring the non almost_trivial Field) by POLYNOM3:def 10;

hence ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) <> {} by A1, XBOOLE_0:def 4; :: thesis: verum

end;<%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> in [#] (Polynom-Ring the non almost_trivial Field) by POLYNOM3:def 10;

hence ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) <> {} by A1, XBOOLE_0:def 4; :: thesis: verum