for S being non void TopStruct holds [#] S is closed_under_lines