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
per cases ( p = q or p <> q ) ;
suppose p = q ; :: thesis: f . p,f . q are_collinear
hence f . p,f . q are_collinear by PENCIL_1:def 1; :: thesis: verum
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;
end;