set M = { f where f is Polynomial of n,R : X c= Zero_ f } ;
A1: { f where f is Polynomial of n,R : X c= Zero_ f } c= [#] (Polynom-Ring (n,R))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { f where f is Polynomial of n,R : X c= Zero_ f } or o in [#] (Polynom-Ring (n,R)) )
assume o in { f where f is Polynomial of n,R : X c= Zero_ f } ; :: thesis: o in [#] (Polynom-Ring (n,R))
then consider x being Polynomial of n,R such that
A3: ( o = x & X c= Zero_ x ) ;
thus o in [#] (Polynom-Ring (n,R)) by A3, POLYNOM1:def 11; :: thesis: verum

end;

{ f where f is Polynomial of n,R : X c= Zero_ f } <> {}

proof

A4: Zero_ (0_ (n,R)) = Funcs (n,([#] R)) by Th13;
0_ (n,R) in { f where f is Polynomial of n,R : X c= Zero_ f } by A4;
hence { f where f is Polynomial of n,R : X c= Zero_ f } <> {} by XBOOLE_0:def 1; :: thesis: verum

end;

hence { f where f is Polynomial of n,R : X c= Zero_ f } is non empty Subset of (Polynom-Ring (n,R)) by A1; :: thesis: verum