let B be Boolean Lattice; :: thesis: Top (B squared-latt) = [(Top B),(Top B)]
[(Top B),(Top B)] in B squared ;
then Top [:B,B:] in B squared by FILTER_1:43;
then Top (latt ([:B,B:],(B squared))) = Top [:B,B:] by ThC;
hence Top (B squared-latt) = [(Top B),(Top B)] by FILTER_1:43; :: thesis: verum