:: deftheorem defines SkelLatt LATSTONE:def 8 :
for L being Stone Lattice holds SkelLatt L = latt (L,(Skeleton L));