consider m being prime Ideal of A such that
A1: J c= m by Th11;
m in PrimeIdeals (A,J) by A1;
hence not PrimeIdeals (A,J) is empty ; :: thesis: verum