let S be non empty TopStruct ; 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; for X being Subset of S st not X is trivial holds
not f " X is trivial
let X be Subset of S; ( not X is trivial implies not f " X is trivial )
assume
not X is trivial
; 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; verum