let S be non empty non void TopStruct ; :: thesis: for f being Collineation of S
for X being Subset of S st X is strong holds
f .: X is strong
let f be Collineation of S; :: thesis: for X being Subset of S st X is strong holds
f .: X is strong
let X be Subset of S; :: thesis: ( X is strong implies f .: X is strong )
assume A1: X is strong ; :: thesis: f .: X is strong
thus f .: X is strong :: thesis: verum

proof

let a, b be Point of S; :: according to PENCIL_1:def 3 :: thesis: ( not a in f .: X or not b in f .: X or a,b are_collinear )
assume that
A2: a in f .: X and
A3: b in f .: X ; :: thesis: a,b are_collinear
thus a,b are_collinear :: thesis: verum

proof

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: a,b are_collinear

hence a,b are_collinear ; :: thesis: verum

end;

suppose A4: a <> b ; :: thesis: a,b are_collinear

consider B being object such that
A5: B in dom f and
A6: B in X and
A7: b = f . B by A3, FUNCT_1:def 6;
consider A being object such that
A8: A in dom f and
A9: A in X and
A10: a = f . A by A2, FUNCT_1:def 6;
reconsider A = A, B = B as Point of S by A8, A5;
A,B are_collinear by A1, A9, A6;
then consider l being Block of S such that
A11: {A,B} c= l by A4, A10, A7;
B in l by A11, ZFMISC_1:32;
then A12: b in f .: l by A5, A7, FUNCT_1:def 6;
A in l by A11, ZFMISC_1:32;
then a in f .: l by A8, A10, FUNCT_1:def 6;
then {a,b} c= f .: l by A12, ZFMISC_1:32;
hence a,b are_collinear ; :: thesis: verum

end;

end;

end;

end;