theorem :: PENCIL_1:22

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