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;

A4: dom f = the carrier of S by FUNCT_2:def 1;

then A5: f . x in f .: X by A1, FUNCT_1:def 6;

A6: f . y in f .: X by A4, A2, FUNCT_1:def 6;

f is bijective by Def4;

then f . x <> f . y by A4, A1, A2, A3, FUNCT_1:def 4;

then 2 c= card (f .: X) by A5, A6, 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;

A4: dom f = the carrier of S by FUNCT_2:def 1;

then A5: f . x in f .: X by A1, FUNCT_1:def 6;

A6: f . y in f .: X by A4, A2, FUNCT_1:def 6;

f is bijective by Def4;

then f . x <> f . y by A4, A1, A2, A3, FUNCT_1:def 4;

then 2 c= card (f .: X) by A5, A6, PENCIL_1:2;

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