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

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;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