theorem Th13: :: PENCIL_2:13

for S being non empty TopStruct
for f being Collineation of S holds f " is Collineation of S