let A be non degenerated commutative Ring; :: thesis: for x being object st x in Spectrum A holds
x is prime Ideal of A
let x be object ; :: thesis: ( x in Spectrum A implies x is prime Ideal of A )
assume x in Spectrum A ; :: thesis: x is prime Ideal of A
then consider x1 being prime Ideal of A such that
A2: x1 = x ;
thus x is prime Ideal of A by A2; :: thesis: verum