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 )
A2: l in the topology of S ;
f is bijective by Def4;
then f is onto ;
then A3: rng f = the carrier of S by FUNCT_2:def 3;
assume 2 c= card (l /\ (f .: X)) ; :: thesis: l c= f .: X
then consider a, b being set such that
A4: ( a in l /\ (f .: X) & b in l /\ (f .: X) & a <> b ) by PENCIL_1:2;
A5: ( a in l & a in f .: X ) by A4, XBOOLE_0:def 4;
then consider A being set such that
A6: ( A in dom f & A in X & a = f . A ) by FUNCT_1:def 12;
A7: ( b in l & b in f .: X ) by A4, XBOOLE_0:def 4;
then consider B being set such that
A8: ( B in dom f & B in X & b = f . B ) by FUNCT_1:def 12;
A in f " l by A5, A6, FUNCT_1:def 13;
then A9: A in (f " l) /\ X by A6, XBOOLE_0:def 4;
B in f " l by A7, A8, FUNCT_1:def 13;
then B in (f " l) /\ X by A8, XBOOLE_0:def 4;
then 2 c= card ((f " l) /\ X) by A4, A6, A8, A9, PENCIL_1:2;
then f " l c= X by A1, PENCIL_1:def 2;
then f .: (f " l) c= f .: X by RELAT_1:156;
hence l c= f .: X by A2, A3, FUNCT_1:147; :: thesis: verum

end;