Top L in Skeleton L by Lm1;
then A0: latt (L,(Skeleton L)) is upper-bounded by ThC;
Bottom L in Skeleton L by Lm1;
then a2: latt (L,(Skeleton L)) is lower-bounded by ThB;
latt (L,(Skeleton L)) is complemented by LattIsComplemented;
hence SkelLatt L is Boolean by a2, A0; :: thesis: verum