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