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

proof

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

end;

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

proof

let x be object ; :: thesis: ( x in { I where I is maximal Ideal of A : verum } implies x in m-Spectrum A )
assume x in { I where I is maximal Ideal of A : verum } ; :: thesis: x in m-Spectrum A
then consider I being maximal Ideal of A such that
A9: I = x ;
I in { I where I is Ideal of A : ( I is quasi-maximal & I <> [#] A ) } ;
hence x in m-Spectrum A by A9, Def4; :: thesis: verum

end;

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