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;
A1: ( the L_meet of DL is idempotent & the L_meet of DL is commutative & the L_meet of DL is associative ) by LATTICE2:30, LATTICE2:31, LATTICE2:32;

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 A1, LATTICE2:35, SETWISEO:37; :: thesis: verum

end;

suppose A2: 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)

A3: 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 A2, 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 A3 ;
:: 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