let S be non empty TopStruct ; :: thesis: for f being Collineation of S

for X being Subset of S st not X is trivial holds

not f " X is trivial

let f be Collineation of S; :: thesis: for X being Subset of S st not X is trivial holds

not f " X is trivial

let X be Subset of S; :: thesis: ( not X is trivial implies not f " X is trivial )

assume not X is trivial ; :: thesis: not f " X is trivial

then 2 c= card X by PENCIL_1:4;

then consider x, y being object such that

A1: x in X and

A2: y in X and

A3: x <> y by PENCIL_1:2;

f is bijective by Def4;

then A4: rng f = the carrier of S by FUNCT_2:def 3;

then consider fx being object such that

A5: fx in dom f and

A6: f . fx = x by A1, FUNCT_1:def 3;

consider fy being object such that

A7: fy in dom f and

A8: f . fy = y by A4, A2, FUNCT_1:def 3;

A9: fy in f " X by A2, A7, A8, FUNCT_1:def 7;

fx in f " X by A1, A5, A6, FUNCT_1:def 7;

then 2 c= card (f " X) by A3, A6, A8, A9, PENCIL_1:2;

hence not f " X is trivial by PENCIL_1:4; :: thesis: verum

for X being Subset of S st not X is trivial holds

not f " X is trivial

let f be Collineation of S; :: thesis: for X being Subset of S st not X is trivial holds

not f " X is trivial

let X be Subset of S; :: thesis: ( not X is trivial implies not f " X is trivial )

assume not X is trivial ; :: thesis: not f " X is trivial

then 2 c= card X by PENCIL_1:4;

then consider x, y being object such that

A1: x in X and

A2: y in X and

A3: x <> y by PENCIL_1:2;

f is bijective by Def4;

then A4: rng f = the carrier of S by FUNCT_2:def 3;

then consider fx being object such that

A5: fx in dom f and

A6: f . fx = x by A1, FUNCT_1:def 3;

consider fy being object such that

A7: fy in dom f and

A8: f . fy = y by A4, A2, FUNCT_1:def 3;

A9: fy in f " X by A2, A7, A8, FUNCT_1:def 7;

fx in f " X by A1, A5, A6, FUNCT_1:def 7;

then 2 c= card (f " X) by A3, A6, A8, A9, PENCIL_1:2;

hence not f " X is trivial by PENCIL_1:4; :: thesis: verum