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

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

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

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

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