let B be Boolean Lattice; DenseElements (B squared-latt) = { [a,(Top B)] where a is Element of B : verum }
set L = B squared-latt ;
thus
DenseElements (B squared-latt) c= { [a,(Top B)] where a is Element of B : verum }
XBOOLE_0:def 10 { [a,(Top B)] where a is Element of B : verum } c= DenseElements (B squared-latt)proof
let x be
object ;
TARSKI:def 3 ( not x in DenseElements (B squared-latt) or x in { [a,(Top B)] where a is Element of B : verum } )
assume
x in DenseElements (B squared-latt)
;
x in { [a,(Top B)] where a is Element of B : verum }
then consider a being
Element of
(B squared-latt) such that A1:
(
x = a &
a * = Bottom (B squared-latt) )
;
x in the
carrier of
(B squared-latt)
by A1;
then
x in B squared
by SquaredCarrier;
then consider a1,
a2 being
Element of
B such that A2:
(
x = [a1,a2] &
a1 [= a2 )
;
A3:
a * = [(Bottom B),(Bottom B)]
by A1, SquaredBottom;
a * = [(a2 `),(a2 `)]
by A1, A2, PseudoInSquared;
then
(a2 `) ` = (Bottom B) `
by A3, XTUPLE_0:1;
then
a2 = Top B
by LATTICE4:30;
hence
x in { [a,(Top B)] where a is Element of B : verum }
by A2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in { [a,(Top B)] where a is Element of B : verum } or x in DenseElements (B squared-latt) )
assume
x in { [a,(Top B)] where a is Element of B : verum }
; x in DenseElements (B squared-latt)
then consider a being Element of B such that
A1:
x = [a,(Top B)]
;
a [= Top B
by LATTICES:19;
then
x in B squared
by A1;
then reconsider y = x as Element of (B squared-latt) by SquaredCarrier;
y * = [((Top B) `),((Top B) `)]
by A1, PseudoInSquared;
then y * =
[(Bottom B),((Top B) `)]
by LATTICE4:29
.=
[(Bottom B),(Bottom B)]
by LATTICE4:29
.=
Bottom (B squared-latt)
by SquaredBottom
;
hence
x in DenseElements (B squared-latt)
; verum