for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f " X is trivial