let S be non empty non void TopStruct ; :: thesis: 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
let f be Collineation of S; :: thesis: for X being Subset of S st X is closed_under_lines holds
f " X is closed_under_lines
reconsider g = f " as Collineation of S by Th13;
let X be Subset of S; :: thesis: ( X is closed_under_lines implies f " X is closed_under_lines )
assume X is closed_under_lines ; :: thesis: f " X is closed_under_lines
then A1: g .: X is closed_under_lines by Th18;
A2: f is bijective by Def4;
then rng f = [#] S by FUNCT_2:def 3;
hence f " X is closed_under_lines by A2, A1, TOPS_2:55; :: thesis: verum