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 ( f is one-to-one & f is onto ) ;
then A1: rng f = the carrier of S by FUNCT_2:def 3;
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
A2: ( x in X & y in X & x <> y ) by PENCIL_1:2;
consider fx being set such that
A3: ( fx in dom f & f . fx = x ) by A1, A2, FUNCT_1:def 5;
consider fy being set such that
A4: ( fy in dom f & f . fy = y ) by A1, A2, FUNCT_1:def 5;
( fx in f " X & fy in f " X ) by A2, A3, A4, FUNCT_1:def 13;
then 2 c= card (f " X) by A2, A3, A4, PENCIL_1:2;
hence not f " X is trivial by PENCIL_1:4; :: thesis: verum