let BL be Boolean Lattice; :: thesis: for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet B,(comp BL)
let B be Finite_Subset of the carrier of BL; :: thesis: (FinJoin B) ` = FinMeet B,(comp BL)
set M = the L_meet of BL;
set J = the L_join of BL;
A1: ( the L_meet of BL is idempotent & the L_meet of BL is commutative & the L_meet of BL is associative & the L_meet of BL is having_a_unity ) by LATTICE2:30, LATTICE2:31, LATTICE2:32, LATTICE2:73;
A2: ( the L_join of BL is idempotent & the L_join of BL is commutative & the L_join of BL is associative & the L_join of BL is having_a_unity ) by LATTICE2:26, LATTICE2:27, LATTICE2:29, LATTICE2:67;
A3: (comp BL) . (the_unity_wrt the L_join of BL) = the_unity_wrt the L_meet of BL

proof

thus (comp BL) . (the_unity_wrt the L_join of BL) = (the_unity_wrt the L_join of BL) ` by Def17
.= (Bottom BL) ` by LATTICE2:68
.= Top BL by Th37
.= the_unity_wrt the L_meet of BL by LATTICE2:74 ; :: thesis: verum

end;

A4: for a, b being Element of BL holds (comp BL) . (the L_join of BL . a,b) = the L_meet of BL . ((comp BL) . a),((comp BL) . b)

proof

let a, b be Element of BL; :: thesis: (comp BL) . (the L_join of BL . a,b) = the L_meet of BL . ((comp BL) . a),((comp BL) . b)
thus (comp BL) . (the L_join of BL . a,b) = (a "\/" b) ` by Def17
.= (a ` ) "/\" (b ` ) by LATTICES:51
.= the L_meet of BL . ((comp BL) . a),(b ` ) by Def17
.= the L_meet of BL . ((comp BL) . a),((comp BL) . b) by Def17 ; :: thesis: verum

end;

thus (FinJoin B) ` = (the L_join of BL $$ B,(id BL)) ` by LATTICE2:def 3
.= (comp BL) . (the L_join of BL $$ B,(id BL)) by Def17
.= the L_meet of BL $$ B,((comp BL) * (id BL)) by A1, A2, A3, A4, SETWISEO:45
.= the L_meet of BL $$ B,(comp BL) by TMAP_1:93
.= FinMeet B,(comp BL) by LATTICE2:def 4 ; :: thesis: verum