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: f .: X is closed_under_lines
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 A3, XBOOLE_0:def 4;
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 A3, XBOOLE_0:def 4;
then B in f " l by A5, A7, FUNCT_1:def 7;
then A8: B in (f " l) /\ X by A6, XBOOLE_0:def 4;
a in f .: X by A2, XBOOLE_0:def 4;
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 A2, XBOOLE_0:def 4;
then A in f " l by A9, A11, FUNCT_1:def 7;
then A in (f " l) /\ X by A10, XBOOLE_0:def 4;
then 2 c= card ((f " l) /\ X) by A4, A11, A7, A8, PENCIL_1:2;
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 A13, A12, FUNCT_1:77; :: thesis: verum

end;