set C = { I where I is Ideal of A : ( I is quasi-prime & I <> [#] A ) } ;
A1: for x being object st x in Spectrum A holds
x in { I where I is prime Ideal of A : verum }

proof

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

end;

for x being object st x in { I where I is prime Ideal of A : verum } holds
x in Spectrum A

proof

let x be object ; :: thesis: ( x in { I where I is prime Ideal of A : verum } implies x in Spectrum A )
assume x in { I where I is prime Ideal of A : verum } ; :: thesis: x in Spectrum A
then consider I being prime Ideal of A such that
A8: I = x ;
reconsider I = I as non empty Subset of A ;
I in { I where I is Ideal of A : ( I is quasi-prime & I <> [#] A ) } ;
hence x in Spectrum A by A8, Def3; :: thesis: verum

end;

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