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

let X be Subset of S; :: thesis: ( X is closed_under_lines implies f .: X is closed_under_lines )
assume A1: X is closed_under_lines ; :: thesis:
thus f .: X is closed_under_lines :: thesis: verum
proof
let l be Block of S; :: according to PENCIL_1:def 2 :: thesis: ( not 2 c= card (l /\ (f .: X)) or l c= f .: X )
assume 2 c= card (l /\ (f .: X)) ; :: thesis: l c= f .: X
then consider a, b being object such that
A2: a in l /\ (f .: X) and
A3: b in l /\ (f .: X) and
A4: a <> b by PENCIL_1:2;
b in f .: X by ;
then consider B being object such that
A5: B in dom f and
A6: B in X and
A7: b = f . B by FUNCT_1:def 6;
b in l by ;
then B in f " l by ;
then A8: B in (f " l) /\ X by ;
a in f .: X by ;
then consider A being object such that
A9: A in dom f and
A10: A in X and
A11: a = f . A by FUNCT_1:def 6;
a in l by ;
then A in f " l by ;
then A in (f " l) /\ X by ;
then 2 c= card ((f " l) /\ X) by ;
then f " l c= X by A1;
then A12: f .: (f " l) c= f .: X by RELAT_1:123;
f is bijective by Def4;
then A13: rng f = the carrier of S by FUNCT_2:def 3;
l in the topology of S ;
hence l c= f .: X by ; :: thesis: verum
end;