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

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