Int ([#] GX) <> {} by Th43;
hence not [#] GX is boundary ; :: thesis: verum