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