let DL be distributive upper-bounded Lattice; :: thesis: for B being Finite_Subset of 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 Finite_Subset of 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 TMAP_1:93
.= FinMeet ((the L_join of DL [:] (id DL),p) .: B) by Th29 ; :: thesis: verum