let DL be distributive upper-bounded Lattice; :: thesis: for B being Finite_Subset of the carrier of DL
for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)
let B be Finite_Subset of the carrier of DL; :: thesis: for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)
let p be Element of DL; :: thesis: for f being UnOp of the carrier of DL holds the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)
let f be UnOp of the carrier of DL; :: thesis: the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)
set J = the L_join of DL;
set M = the L_meet of DL;

now

per cases ( B <> {} or B = {} ) ;

suppose B <> {} ; :: thesis: the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)

hence the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p) by LATTICE2:35, SETWISEO:37; :: thesis: verum

end;

suppose A3: B = {} ; :: thesis: the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)

A4: now

let f be UnOp of the carrier of DL; :: thesis: the L_meet of DL $$ B,f = Top DL
thus the L_meet of DL $$ B,f = FinMeet ({}. the carrier of DL),f by A3, LATTICE2:def 4
.= Top DL by Lm2 ; :: thesis: verum

end;

hence the L_join of DL . (the L_meet of DL $$ B,f),p = (Top DL) "\/" p
.= Top DL by LATTICES:44
.= the L_meet of DL $$ B,(the L_join of DL [:] f,p) by A4 ;
:: thesis: verum

end;

end;

end;

hence the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p) ; :: thesis: verum