:: deftheorem defines OpenClosedSetLatt LOPCLSET:def 4 :
for T being non empty TopSpace holds OpenClosedSetLatt T = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);