:: deftheorem defines Skeleton LATSTONE:def 4 :
for L being lower-bounded pseudocomplemented Lattice holds Skeleton L = { (a *) where a is Element of L : verum } ;