let B be Boolean Lattice; :: thesis: Skeleton (B squared-latt) = { [a,a] where a is Element of B : verum }
set L = B squared-latt ;
Skeleton (B squared-latt) = { [a,a] where a is Element of B : verum }

proof

thus Skeleton (B squared-latt) c= { [a,a] where a is Element of B : verum } :: according to XBOOLE_0:def 10 :: thesis: { [a,a] where a is Element of B : verum } c= Skeleton (B squared-latt)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Skeleton (B squared-latt) or x in { [a,a] where a is Element of B : verum } )
assume x in Skeleton (B squared-latt) ; :: thesis: x in { [a,a] where a is Element of B : verum }
then consider a being Element of (B squared-latt) such that
A1: x = a * ;
a in the carrier of (B squared-latt) ;
then a in B squared by SquaredCarrier;
then consider a1, a2 being Element of B such that
A2: ( a = [a1,a2] & a1 [= a2 ) ;
a * = [(a2 `),(a2 `)] by A2, PseudoInSquared;
hence x in { [a,a] where a is Element of B : verum } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [a,a] where a is Element of B : verum } or x in Skeleton (B squared-latt) )
assume x in { [a,a] where a is Element of B : verum } ; :: thesis: x in Skeleton (B squared-latt)
then consider a being Element of B such that
B1: x = [a,a] ;
set b = [(a `),(a `)];
[(a `),(a `)] in B squared ;
then reconsider b = [(a `),(a `)] as Element of (B squared-latt) by FILTER_2:72;
reconsider a1 = b * as Element of (B squared-latt) ;
b * = [((a `) `),((a `) `)] by PseudoInSquared
.= [a,a] ;
hence x in Skeleton (B squared-latt) by B1; :: thesis: verum

end;

hence Skeleton (B squared-latt) = { [a,a] where a is Element of B : verum } ; :: thesis: verum