let DL be distributive upper-bounded Lattice; :: thesis: for B being Element of Fin 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 Element of Fin 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;

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 Element of Fin 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 :: 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)))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: verumper cases
( B <> {} or B = {} )
;

end;

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:21, SETWISEO:28; :: thesis: verum

end;suppose A1:
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)))

.= Top DL

.= the L_meet of DL $$ (B,( the L_join of DL [:] (f,p))) by A2 ;

:: thesis: verum

end;

A2: now :: thesis: for f being UnOp of the carrier of DL holds the L_meet of DL $$ (B,f) = Top DL

hence the L_join of DL . (( the L_meet of DL $$ (B,f)),p) =
(Top DL) "\/" p
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 A1, LATTICE2:def 4

.= Top DL by Lm2 ; :: thesis: verum

end;thus the L_meet of DL $$ (B,f) = FinMeet (({}. the carrier of DL),f) by A1, LATTICE2:def 4

.= Top DL by Lm2 ; :: thesis: verum

.= Top DL

.= the L_meet of DL $$ (B,( the L_join of DL [:] (f,p))) by A2 ;

:: thesis: verum