let L be Stone Lattice; :: thesis: ( Bottom L = Bottom (SkelLatt L) & Top L = Top (SkelLatt L) )
( Bottom L in Skeleton L & Top L in Skeleton L ) by Lm1;
hence ( Bottom L = Bottom (SkelLatt L) & Top L = Top (SkelLatt L) ) by ThB, ThC; :: thesis: verum