let BL be non trivial B_Lattice; :: thesis: for a being Element of BL

for F being Filter of BL holds

( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

let a be Element of BL; :: thesis: for F being Filter of BL holds

( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

let F be Filter of BL; :: thesis: ( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

for F being Filter of BL holds

( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

let a be Element of BL; :: thesis: for F being Filter of BL holds

( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

let F be Filter of BL; :: thesis: ( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

hereby :: thesis: ( F is being_ultrafilter & a in F implies F in (UFilter BL) . a )

thus
( F is being_ultrafilter & a in F implies F in (UFilter BL) . a )
by Th17; :: thesis: verumassume
F in (UFilter BL) . a
; :: thesis: ( F is being_ultrafilter & a in F )

then ex F0 being Filter of BL st

( F0 = F & F0 is being_ultrafilter & a in F0 ) by Th17;

hence ( F is being_ultrafilter & a in F ) ; :: thesis: verum

end;then ex F0 being Filter of BL st

( F0 = F & F0 is being_ultrafilter & a in F0 ) by Th17;

hence ( F is being_ultrafilter & a in F ) ; :: thesis: verum