for DL being distributive upper-bounded Lattice
for B being Element of Fin the carrier of DL
for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)