Bottom [:B,B:] = [(Bottom B),(Bottom B)] by FILTER_1:42;
then Bottom [:B,B:] in B squared ;
hence B squared-latt is lower-bounded by ThB; :: thesis: verum