let B be Boolean Lattice; :: thesis: the carrier of (B squared-latt) = B squared
set L = [:B,B:];
set P = B squared ;
consider o1, o2 being BinOp of (B squared) such that
A1: ( o1 = the L_join of [:B,B:] || (B squared) & o2 = the L_meet of [:B,B:] || (B squared) & latt ([:B,B:],(B squared)) = LattStr(# (B squared),o1,o2 #) ) by FILTER_2:def 14;
thus the carrier of (B squared-latt) = B squared by A1; :: thesis: verum