let BL be Boolean Lattice; for B being Element of Fin the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))
let B be Element of Fin the carrier of BL; (FinJoin B) ` = FinMeet (B,(comp BL))
set M = the L_meet of BL;
set J = the L_join of BL;
A1:
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))
A2: (comp BL) . (the_unity_wrt the L_join of BL) =
(the_unity_wrt the L_join of BL) `
by Def12
.=
(Bottom BL) `
by LATTICE2:52
.=
Top BL
by Th30
.=
the_unity_wrt the L_meet of BL
by LATTICE2:57
;
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 Def12
.=
the L_meet of BL $$ (B,((comp BL) * (id BL)))
by A2, A1, SETWISEO:36
.=
the L_meet of BL $$ (B,(comp BL))
by FUNCT_2:17
.=
FinMeet (B,(comp BL))
by LATTICE2:def 4
; verum