set X = { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } ;
thus ( not R is degenerated implies { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } is Subset of (Spectrum R) ) :: thesis: ( R is degenerated implies {} is Subset of (Spectrum R) )

proof

assume A1: not R is degenerated ; :: thesis: { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } is Subset of (Spectrum R)
{ p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } c= Spectrum R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } or x in Spectrum R )
assume x in { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } ; :: thesis: x in Spectrum R
then consider p being Ideal of R such that
A3: x = p and
A4: p is quasi-prime and
A5: p <> [#] R and
E c= p ;
p in { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R ) } by A4, A5;
hence x in Spectrum R by A3, A1, Def3; :: thesis: verum

end;

hence { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } is Subset of (Spectrum R) ; :: thesis: verum

end;

thus ( R is degenerated implies {} is Subset of (Spectrum R) ) by XBOOLE_1:2; :: thesis: verum