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