let A be non degenerated commutative Ring; :: thesis: for p being prime Ideal of A
for n being non zero Nat holds p ||^ n is proper
let p be prime Ideal of A; :: thesis: for n being non zero Nat holds p ||^ n is proper
let n be non zero Nat; :: thesis: p ||^ n is proper
assume A1: not p ||^ n is proper ; :: thesis: contradiction
p = sqrt (p ||^ n) by Th15
.= [#] A by A1, Th13 ;
hence contradiction ; :: thesis: verum