:: deftheorem Def13 defines Sublattice FILTER_2:def 13 :
for L being Lattice
for b₂ being LattStr holds
( b₂ is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b₂, the L_join of b₂, the L_meet of b₂ #) = LattStr(# P,o1,o2 #) ) );