let A be non degenerated commutative Ring; :: thesis: for a being Element of A st a is NonUnit of A holds
ex m being maximal Ideal of A st a in m
let a be Element of A; :: thesis: ( a is NonUnit of A implies ex m being maximal Ideal of A st a in m )
assume a is NonUnit of A ; :: thesis: ex m being maximal Ideal of A st a in m
then {a} -Ideal <> [#] A by RING_2:20;
then {a} -Ideal is proper ;
then consider m being maximal Ideal of A such that
A2: {a} -Ideal c= m by Th10;
a in m by A2, IDEAL_1:66;
hence ex m being maximal Ideal of A st a in m ; :: thesis: verum