:: deftheorem Def14 defines latt FILTER_2:def 14 :
for L being Lattice
for P being non empty ClosedSubset of L
for b₃ being Sublattice of L holds
( b₃ = latt (L,P) iff ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b₃ = LattStr(# P,o1,o2 #) ) );