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