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 b1 being Subset-Family of A holds
( b1 = Spectrum A iff b1 = { I where I is prime Ideal of A : verum } ) ) ) by TARSKI:2, A1; :: thesis: verum