let A be non degenerated commutative Ring; :: thesis: for P being Point of (ZariskiTS A) holds P is prime Ideal of A
let P be Point of (ZariskiTS A); :: thesis: P is prime Ideal of A
P in [#] (ZariskiTS A) ;
then P in Spectrum A by Def7;
hence P is prime Ideal of A by Th22; :: thesis: verum