reconsider p = p as prime Ideal of A by Lm5;
0. A in p by IDEAL_1:3;
then not 0. A in ([#] A) \ p by XBOOLE_0:def 5;
hence not A ~ p is degenerated by Th31; :: thesis: verum