:: deftheorem defines Open_setLatt OPENLATT:def 4 :
for T being non empty TopSpace holds Open_setLatt T = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);