for L being Lattice
for P being non empty ClosedSubset of L
for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) by Th1, Th5, LATTICE2:26, LATTICE2:27;