let S be non empty non void TopStruct ; 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; for X being Subset of S st X is strong holds
f .: X is strong
let X be Subset of S; ( X is strong implies f .: X is strong )
assume A1:
X is strong
; f .: X is strong
thus
f .: X is strong
verumproof
let a,
b be
Point of
S;
PENCIL_1:def 3 ( 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
;
a,b are_collinear
thus
a,
b are_collinear
verumproof
per cases
( a = b or a <> b )
;
suppose A4:
a <> b
;
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
;
verum end;
end;
end;