set L = B squared-latt ;
for x being Element of (B squared-latt) holds (x *) "\/" ((x *) *) = Top (B squared-latt)

proof

let x be Element of (B squared-latt); :: thesis: (x *) "\/" ((x *) *) = Top (B squared-latt)
x in the carrier of (B squared-latt) ;
then x in B squared by SquaredCarrier;
then consider x1, x2 being Element of B such that
W1: ( x = [x1,x2] & x1 [= x2 ) ;
[(x2 `),(x2 `)] in B squared ;
then reconsider y = [(x2 `),(x2 `)] as Element of (B squared-latt) by SquaredCarrier;
W0: x * = [(x2 `),(x2 `)] by W1, PseudoInSquared;
then (x *) * = [((x2 `) `),((x2 `) `)] by PseudoInSquared;
then (x *) "\/" ((x *) *) = [(x2 `),(x2 `)] "\/" [x2,x2] by W0, MSUALG_7:11
.= [((x2 `) "\/" x2),((x2 `) "\/" x2)] by FILTER_1:35
.= [(Top B),((x2 `) "\/" x2)] by LATTICES:21
.= [(Top B),(Top B)] by LATTICES:21
.= Top (B squared-latt) by SquaredTop ;
hence (x *) "\/" ((x *) *) = Top (B squared-latt) ; :: thesis: verum

end;

hence B squared-latt is satisfying_Stone_identity ; :: thesis: verum