set C = { p where p is Ideal of A : ( p is quasi-prime & p <> [#] A & E c= p ) } ;
A1: for x being object st x in PrimeIdeals (A,E) holds
x in { p where p is prime Ideal of A : E c= p }

proof

let x be object ; :: thesis: ( x in PrimeIdeals (A,E) implies x in { p where p is prime Ideal of A : E c= p } )
assume x in PrimeIdeals (A,E) ; :: thesis: x in { p where p is prime Ideal of A : E c= p }
then A3: x in { p where p is Ideal of A : ( p is quasi-prime & p <> [#] A & E c= p ) } by Def5;
consider I being Ideal of A such that
A4: x = I and
A5: I is quasi-prime and
A6: I <> [#] A and
A7: E c= I by A3;
reconsider I = I as prime Ideal of A by A5, A6, RING_1:def 2, SUBSET_1:def 6;
I in { p where p is prime Ideal of A : E c= p } by A7;
hence x in { p where p is prime Ideal of A : E c= p } by A4; :: thesis: verum

end;

for x being object st x in { p where p is prime Ideal of A : E c= p } holds
x in PrimeIdeals (A,E)

proof

let x be object ; :: thesis: ( x in { p where p is prime Ideal of A : E c= p } implies x in PrimeIdeals (A,E) )
assume x in { p where p is prime Ideal of A : E c= p } ; :: thesis: x in PrimeIdeals (A,E)
then consider I being prime Ideal of A such that
A9: I = x and
A10: E c= I ;
I in { p where p is Ideal of A : ( p is quasi-prime & p <> [#] A & E c= p ) } by A10;
hence x in PrimeIdeals (A,E) by A9, Def5; :: thesis: verum

end;

hence ( PrimeIdeals (A,E) is Subset of (Spectrum A) & ( for b₁ being Subset of (Spectrum A) holds
( b₁ = PrimeIdeals (A,E) iff b₁ = { p where p is prime Ideal of A : E c= p } ) ) ) by TARSKI:2, A1; :: thesis: verum