theorem :: LOPCLSET:12

for T being non empty TopSpace holds the carrier of (OpenClosedSetLatt T) = OpenClosedSet T ;