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;
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; verum