let B be Boolean Lattice; 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 }
XBOOLE_0:def 10 { [a,a] where a is Element of B : verum } c= Skeleton (B squared-latt)
let x be
object ;
TARSKI:def 3 ( 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 }
;
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;
verum
end;
hence
Skeleton (B squared-latt) = { [a,a] where a is Element of B : verum }
; verum