let B be Boolean Lattice; 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; 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; for x being Element of L st L = B squared-latt & x = [x1,x2] holds
x * = [(x2 `),(x2 `)]
let x be Element of L; ( L = B squared-latt & x = [x1,x2] implies x * = [(x2 `),(x2 `)] )
assume A0:
( L = B squared-latt & x = [x1,x2] )
; 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;
( x "/\" w = Bottom L implies w [= y )
assume O1:
x "/\" w = Bottom L
;
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;
verum
end;
then
y is_a_pseudocomplement_of x
by tt, Z1, A0, SquaredBottom;
hence
x * = [(x2 `),(x2 `)]
by def3, A0; verum