set L = B squared-latt ;
for x being Element of (B squared-latt) ex y being Element of (B squared-latt) st y is_a_pseudocomplement_of x

proof

let x be Element of (B squared-latt); :: thesis: ex y being Element of (B squared-latt) st y is_a_pseudocomplement_of x
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
A1: ( x = [x1,x2] & x1 [= x2 ) ;
I1: [(x2 `),(x2 `)] in B squared ;
reconsider y = [(x2 `),(x2 `)] as Element of (B squared-latt) by I1, SquaredCarrier;
take y ; :: thesis: y is_a_pseudocomplement_of x
Z1: x "/\" y = [x1,x2] "/\" [(x2 `),(x2 `)] by A1, MSUALG_7:11
.= [(x1 "/\" (x2 `)),(x2 "/\" (x2 `))] by FILTER_1:35
.= [(x1 "/\" (x2 `)),(Bottom B)] by LATTICES:20 ;
x2 ` [= x1 ` by A1, LATTICES:26;
then x1 "/\" (x2 `) [= x1 "/\" (x1 `) by FILTER_0:5;
then x1 "/\" (x2 `) [= Bottom B by LATTICES:20;
then tt: x1 "/\" (x2 `) = Bottom B by BOOLEALG:9;
for w being Element of (B squared-latt) st x "/\" w = Bottom (B squared-latt) holds
w [= y

proof

let w be Element of (B squared-latt); :: thesis: ( x "/\" w = Bottom (B squared-latt) implies w [= y )
assume O1: x "/\" w = Bottom (B squared-latt) ; :: thesis: w [= y
w in the carrier of (B squared-latt) ;
then w in B squared by SquaredCarrier;
then consider w1, w2 being Element of B such that
Y1: ( w = [w1,w2] & w1 [= w2 ) ;
[x1,x2] "/\" [w1,w2] = Bottom (B squared-latt) by O1, Y1, A1, MSUALG_7:11;
then [x1,x2] "/\" [w1,w2] = [(Bottom B),(Bottom B)] by SquaredBottom;
then [(x1 "/\" w1),(x2 "/\" w2)] = [(Bottom B),(Bottom B)] by FILTER_1:35;
then ( x1 "/\" w1 = Bottom B & x2 "/\" w2 = Bottom B ) by XTUPLE_0:1;
then Y2: w2 [= x2 ` by LATTICES:25;
then w1 [= x2 ` by Y1, LATTICES:7;
then [w1,w2] "/\" [(x2 `),(x2 `)] = [w1,w2] by LATTICES:4, Y2, FILTER_1:36;
then w "/\" y = w by Y1, MSUALG_7:11;
hence w [= y by LATTICES:4; :: thesis: verum

end;

hence y is_a_pseudocomplement_of x by tt, Z1, SquaredBottom; :: thesis: verum

end;

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