:: deftheorem defines OpenClosedSet LOPCLSET:def 1 :
for T being non empty TopStruct holds OpenClosedSet T = { x where x is Subset of T : ( x is open & x is closed ) } ;