let L be lower-bounded pseudocomplemented Lattice; :: thesis: Skeleton L = { a where a is Element of L : (a *) * = a }
thus Skeleton L c= { a where a is Element of L : (a *) * = a } :: according to XBOOLE_0:def 10 :: thesis: { a where a is Element of L : (a *) * = a } c= Skeleton L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Skeleton L or x in { a where a is Element of L : (a *) * = a } )
assume x in Skeleton L ; :: thesis: x in { a where a is Element of L : (a *) * = a }
then consider a being Element of L such that
a1: x = a * ;
((a *) *) * = a * by Th7;
hence x in { a where a is Element of L : (a *) * = a } by a1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of L : (a *) * = a } or x in Skeleton L )
assume x in { a where a is Element of L : (a *) * = a } ; :: thesis: x in Skeleton L
then consider a being Element of L such that
a3: ( x = a & (a *) * = a ) ;
thus x in Skeleton L by a3; :: thesis: verum