let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A
for x being object st x in I & I is proper Ideal of A holds
x is NonUnit of A
let I be Ideal of A; :: thesis: for x being object st x in I & I is proper Ideal of A holds
x is NonUnit of A
let x be object ; :: thesis: ( x in I & I is proper Ideal of A implies x is NonUnit of A )
assume that
A1: x in I and
A2: I is proper Ideal of A ; :: thesis: x is NonUnit of A
assume A3: x is not NonUnit of A ; :: thesis: contradiction
reconsider x = x as Element of A by A1;
{x} -Ideal = [#] A by A3, RING_2:20;
then [#] A = I by A1, RING_2:4;
hence contradiction by A2; :: thesis: verum