let A be non degenerated commutative Ring; :: thesis: for o being object st o in Spectrum A holds
o is prime Ideal of A
let o be object ; :: thesis: ( o in Spectrum A implies o is prime Ideal of A )
assume o in Spectrum A ; :: thesis: o is prime Ideal of A
then o in { I where I is Ideal of A : ( I is quasi-prime & I <> [#] A ) } by TOPZARI1:def 5;
then consider o1 being Ideal of A such that
A1: ( o1 = o & o1 is quasi-prime & o1 <> [#] A ) ;
o1 is proper Ideal of A by A1, SUBSET_1:def 6;
hence o is prime Ideal of A by A1; :: thesis: verum