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

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

proof

hence
{ F where F is Filter of BL : F is being_ultrafilter } is Subset-Family of BL
; :: thesis: verum
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;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