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:
thus a,b are_collinear :: thesis: verum
proof
per cases ( a = b or a <> b ) ;
suppose A4: a <> b ; :: thesis:
consider B being object such that
A5: B in dom f and
A6: B in X and
A7: b = f . B by ;
consider A being object such that
A8: A in dom f and
A9: A in X and
A10: a = f . A by ;
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 ;
then A12: b in f .: l by ;
A in l by ;
then a in f .: l by ;
then {a,b} c= f .: l by ;
hence a,b are_collinear ; :: thesis: verum
end;
end;
end;
end;