let A be non degenerated commutative Ring; :: thesis: PrimeIdeals (A,{(1. A)}) = {}
assume PrimeIdeals (A,{(1. A)}) <> {} ; :: thesis: contradiction
then consider p being object such that
A2: p in PrimeIdeals (A,{(1. A)}) by XBOOLE_0:def 1;
consider p1 being prime Ideal of A such that
p1 = p and
A3: {(1. A)} c= p1 by A2;
1. A in {(1. A)} by TARSKI:def 1;
hence contradiction by A3, IDEAL_1:19; :: thesis: verum