thus ( not R is degenerated implies { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } is Subset of (bool the carrier of R) ) :: thesis: ( R is degenerated implies {} is Subset-Family of R )

proof

set X = { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } ;
{ I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } c= bool the carrier of R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } or x in bool the carrier of R )
assume x in { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } ; :: thesis: x in bool the carrier of R
then ex I being Ideal of R st
( x = I & I is quasi-maximal & I <> [#] R ) ;
hence x in bool the carrier of R ; :: thesis: verum

end;

hence ( not R is degenerated implies { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } is Subset of (bool the carrier of R) ) ; :: thesis: verum

end;

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