let S be non empty non void TopStruct ; :: thesis: for f being Collineation of S

for p, q being Point of S st p,q are_collinear holds

f . p,f . q are_collinear

let f be Collineation of S; :: thesis: for p, q being Point of S st p,q are_collinear holds

f . p,f . q are_collinear

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

let p, q be Point of S; :: thesis: ( p,q are_collinear implies f . p,f . q are_collinear )

assume A2: p,q are_collinear ; :: thesis: f . p,f . q are_collinear

for p, q being Point of S st p,q are_collinear holds

f . p,f . q are_collinear

let f be Collineation of S; :: thesis: for p, q being Point of S st p,q are_collinear holds

f . p,f . q are_collinear

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

let p, q be Point of S; :: thesis: ( p,q are_collinear implies f . p,f . q are_collinear )

assume A2: p,q are_collinear ; :: thesis: f . p,f . q are_collinear

per cases
( p = q or p <> q )
;

end;

suppose
p <> q
; :: thesis: f . p,f . q are_collinear

then consider B being Block of S such that

A3: {p,q} c= B by A2, PENCIL_1:def 1;

q in B by A3, ZFMISC_1:32;

then A4: f . q in f .: B by A1, FUNCT_1:def 6;

p in B by A3, ZFMISC_1:32;

then f . p in f .: B by A1, FUNCT_1:def 6;

then {(f . p),(f . q)} c= f .: B by A4, ZFMISC_1:32;

hence f . p,f . q are_collinear by PENCIL_1:def 1; :: thesis: verum

end;A3: {p,q} c= B by A2, PENCIL_1:def 1;

q in B by A3, ZFMISC_1:32;

then A4: f . q in f .: B by A1, FUNCT_1:def 6;

p in B by A3, ZFMISC_1:32;

then f . p in f .: B by A1, FUNCT_1:def 6;

then {(f . p),(f . q)} c= f .: B by A4, ZFMISC_1:32;

hence f . p,f . q are_collinear by PENCIL_1:def 1; :: thesis: verum