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 ;

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)%> ) ;

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;

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;

end;