for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f .: X is closed_under_lines