Top [:B,B:] = [(Top B),(Top B)] by FILTER_1:43;
then Top [:B,B:] in B squared ;
hence B squared-latt is upper-bounded by ThC; :: thesis: verum