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 )
f is bijective by Def4;
then A1: f is one-to-one ;
A2: dom f = the carrier of S by FUNCT_2:def 1;
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 set such that
A3: ( x in X & y in X & x <> y ) by PENCIL_1:2;
A4: ( f . x in f .: X & f . y in f .: X ) by A2, A3, FUNCT_1:def 12;
f . x <> f . y by A1, A2, A3, FUNCT_1:def 8;
then 2 c= card (f .: X) by A4, PENCIL_1:2;
hence not f .: X is trivial by PENCIL_1:4; :: thesis: verum