Int ([#] T) = [#] T by Th43;
hence [#] T is open ; :: thesis: verum