let DL be distributive upper-bounded Lattice; :: thesis: 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)
let B be Element of Fin the carrier of DL; :: thesis: for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
let p be Element of DL; :: thesis: (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
set J = the L_join of DL;
set M = the L_meet of DL;
thus (FinMeet B) "\/" p = the L_join of DL . (( the L_meet of DL $$ (B,(id DL))),p) by LATTICE2:def 4
.= the L_meet of DL $$ (B,( the L_join of DL [:] ((id DL),p))) by Lm3
.= FinMeet (B,( the L_join of DL [:] ((id DL),p))) by LATTICE2:def 4
.= FinMeet (B,((id DL) * ( the L_join of DL [:] ((id DL),p)))) by FUNCT_2:17
.= FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) by Th22 ; :: thesis: verum