:: deftheorem Def9 defines latt FILTER_0:def 9 :
for L being Lattice
for F being Filter of L
for b₃ being Lattice holds
( b₃ = latt F iff ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b₃ = LattStr(# F,o1,o2 #) ) );