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

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