set US = { F where F is Filter of BL : F is being_ultrafilter } ;
{ F where F is Filter of BL : F is being_ultrafilter } c= bool the carrier of BL

proof

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

end;

hence { F where F is Filter of BL : F is being_ultrafilter } is Subset-Family of BL ; :: thesis: verum