let BL be non trivial B_Lattice; :: thesis: for a, b being Element of BL
for F being Filter of BL st F is being_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
let a, b be Element of BL; :: thesis: for F being Filter of BL st F is being_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
let F be Filter of BL; :: thesis: ( F is being_ultrafilter implies ( a "\/" b in F iff ( a in F or b in F ) ) )
assume F is being_ultrafilter ; :: thesis: ( a "\/" b in F iff ( a in F or b in F ) )
then F is prime by FILTER_0:45;
hence ( a "\/" b in F iff ( a in F or b in F ) ) by FILTER_0:def 5; :: thesis: verum