let BL be non trivial B_Lattice; :: thesis: for a being Element of BL holds { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } c= ultraset BL

let a be Element of BL; :: thesis: { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } c= ultraset BL

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } or x in ultraset BL )

assume x in { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } ; :: thesis: x in ultraset BL

then ex UF being Filter of BL st

( UF = x & UF is being_ultrafilter & a in UF ) ;

hence x in ultraset BL ; :: thesis: verum

let a be Element of BL; :: thesis: { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } c= ultraset BL

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } or x in ultraset BL )

assume x in { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } ; :: thesis: x in ultraset BL

then ex UF being Filter of BL st

( UF = x & UF is being_ultrafilter & a in UF ) ;

hence x in ultraset BL ; :: thesis: verum