set US = { F where F is Ideal of L : ( F is prime & F is proper ) } ;
{ F where F is Ideal of L : ( F is prime & F is proper ) } c= bool the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Ideal of L : ( F is prime & F is proper ) } or x in bool the carrier of L )
assume x in { F where F is Ideal of L : ( F is prime & F is proper ) } ; :: thesis: x in bool the carrier of L
then ex UF being Ideal of L st
( UF = x & UF is prime & UF is proper ) ;
hence x in bool the carrier of L ; :: thesis: verum

end;

hence { I where I is Ideal of L : ( I is prime & I is proper ) } is Subset-Family of L ; :: thesis: verum