:: deftheorem defines StoneLatt OPENLATT:def 11 :
for L being D_Lattice holds StoneLatt L = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);