let B be Boolean Lattice; :: thesis: [(Top B),(Top B)] in the carrier of (B squared-latt)
[(Top B),(Top B)] in B squared ;
hence [(Top B),(Top B)] in the carrier of (B squared-latt) by SquaredCarrier; :: thesis: verum