for L being Lattice
for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )