let B be Boolean Lattice; :: thesis: 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 } :: according to XBOOLE_0:def 10 :: thesis: { [a,(Top B)] where a is Element of B : verum } c= DenseElements (B squared-latt)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: 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) ; :: thesis: verum