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