let B be Boolean Lattice; :: thesis: for L being Lattice
for x1, x2 being Element of B
for x being Element of L st L = B squared-latt & x = [x1,x2] holds
x * = [(x2 `),(x2 `)]
let L be Lattice; :: thesis: for x1, x2 being Element of B
for x being Element of L st L = B squared-latt & x = [x1,x2] holds
x * = [(x2 `),(x2 `)]
let x1, x2 be Element of B; :: thesis: for x being Element of L st L = B squared-latt & x = [x1,x2] holds
x * = [(x2 `),(x2 `)]
let x be Element of L; :: thesis: ( L = B squared-latt & x = [x1,x2] implies x * = [(x2 `),(x2 `)] )
assume A0: ( L = B squared-latt & x = [x1,x2] ) ; :: thesis: x * = [(x2 `),(x2 `)]
x in the carrier of L ;
then x in B squared by SquaredCarrier, A0;
then consider xx1, xx2 being Element of B such that
W1: ( x = [xx1,xx2] & xx1 [= xx2 ) ;
aa: ( xx1 = x1 & xx2 = x2 ) by W1, A0, XTUPLE_0:1;
[(x2 `),(x2 `)] in B squared ;
then reconsider y = [(x2 `),(x2 `)] as Element of L by A0, SquaredCarrier;
Z1: x "/\" y = [x1,x2] "/\" [(x2 `),(x2 `)] by A0, MSUALG_7:11
.= [(x1 "/\" (x2 `)),(x2 "/\" (x2 `))] by FILTER_1:35
.= [(x1 "/\" (x2 `)),(Bottom B)] by LATTICES:20 ;
x2 ` [= x1 ` by aa, W1, 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 L st x "/\" w = Bottom L holds
w [= y

proof

let w be Element of L; :: thesis: ( x "/\" w = Bottom L implies w [= y )
assume O1: x "/\" w = Bottom L ; :: thesis: w [= y
w in the carrier of L ;
then w in B squared by A0, SquaredCarrier;
then consider w1, w2 being Element of B such that
Y1: ( w = [w1,w2] & w1 [= w2 ) ;
[x1,x2] "/\" [w1,w2] = Bottom L by O1, Y1, A0, MSUALG_7:11;
then [x1,x2] "/\" [w1,w2] = [(Bottom B),(Bottom B)] by A0, 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, A0;
hence w [= y by LATTICES:4; :: thesis: verum

end;

then y is_a_pseudocomplement_of x by tt, Z1, A0, SquaredBottom;
hence x * = [(x2 `),(x2 `)] by def3, A0; :: thesis: verum