let B be Boolean Lattice; :: thesis: Bottom (B squared-latt) = [(Bottom B),(Bottom B)]
[(Bottom B),(Bottom B)] in B squared ;
then Bottom [:B,B:] in B squared by FILTER_1:42;
then Bottom (latt ([:B,B:],(B squared))) = Bottom [:B,B:] by ThB;
hence Bottom (B squared-latt) = [(Bottom B),(Bottom B)] by FILTER_1:42; :: thesis: verum