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