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

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