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 ) )

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

assume 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;

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