let CPS be proper CollSp; for p, q being POINT of ex P being LINE of st
( p on P & q on P )
let p, q be POINT of ; ex P being LINE of st
( p on P & q on P )
reconsider p' = p, q' = q as Point of ;
A1:
now consider r' being
Point of
such that A2:
p' <> r'
by Th11;
consider P' being
LINE of
CPS such that A3:
p' in P'
and
r' in P'
by A2, COLLSP:24;
reconsider P =
P' as
LINE of
by Th2;
assume A4:
p' = q'
;
ex P being LINE of st
( p on P & q on P )
p on P
by A3, Th9;
hence
ex
P being
LINE of st
(
p on P &
q on P )
by A4;
verum end;
now assume
p' <> q'
;
ex P being LINE of st
( p on P & q on P )then consider P' being
LINE of
CPS such that A5:
(
p' in P' &
q' in P' )
by COLLSP:24;
reconsider P =
P' as
LINE of
by Th2;
(
p on P &
q on P )
by A5, Th9;
hence
ex
P being
LINE of st
(
p on P &
q on P )
;
verum end;
hence
ex P being LINE of st
( p on P & q on P )
by A1; verum