let L be Lattice; :: thesis: 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 )
let P be non empty ClosedSubset of L; :: thesis: 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 )
let o1, o2 be BinOp of P; :: thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P implies ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) )
( H₂(L) absorbs H₃(L) & H₃(L) absorbs H₂(L) ) by LATTICE2:26, LATTICE2:27;
hence ( o1 = the L_join of L || P & o2 = the L_meet of L || P implies ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) ) by Th1, Th5; :: thesis: verum