let BL be Boolean Lattice; :: thesis: for B being Element of Fin the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL))
let B be Element of Fin the carrier of BL; :: thesis: (FinMeet B) ` = FinJoin (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_meet of BL . (a,b)) = the L_join of BL . (((comp BL) . a),((comp BL) . b))
proof
let a, b be Element of BL; :: thesis: (comp BL) . ( the L_meet of BL . (a,b)) = the L_join of BL . (((comp BL) . a),((comp BL) . b))
thus (comp BL) . ( the L_meet of BL . (a,b)) = (a "/\" b) ` by Def12
.= (a `) "\/" (b `) by LATTICES:23
.= the L_join of BL . (((comp BL) . a),(b `)) by Def12
.= the L_join of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; :: thesis: verum
end;
A2: (comp BL) . (the_unity_wrt the L_meet of BL) = (the_unity_wrt the L_meet of BL) ` by Def12
.= (Top BL) ` by LATTICE2:57
.= Bottom BL by Th29
.= the_unity_wrt the L_join of BL by LATTICE2:52 ;
thus (FinMeet B) ` = ( the L_meet of BL $$ (B,(id BL))) ` by LATTICE2:def 4
.= (comp BL) . ( the L_meet of BL $$ (B,(id BL))) by Def12
.= the L_join of BL $$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36
.= the L_join of BL $$ (B,(comp BL)) by FUNCT_2:17
.= FinJoin (B,(comp BL)) by LATTICE2:def 3 ; :: thesis: verum