let CLSP be proper CollSp; for p, q, r being Point of CLSP
for P being LINE of CLSP st p in P & q in P & r in P holds
p,q,r are_collinear
let p, q, r be Point of CLSP; for P being LINE of CLSP st p in P & q in P & r in P holds
p,q,r are_collinear
let P be LINE of CLSP; ( p in P & q in P & r in P implies p,q,r are_collinear )
assume that
A1:
( p in P & q in P )
and
A2:
r in P
; p,q,r are_collinear
consider a, b being Point of CLSP such that
A3:
a <> b
and
A4:
P = Line (a,b)
by Def7;
A5:
ex z being Point of CLSP st
( z = r & a,b,z are_collinear )
by A2, A4;
( ex x being Point of CLSP st
( x = p & a,b,x are_collinear ) & ex y being Point of CLSP st
( y = q & a,b,y are_collinear ) )
by A1, A4;
hence
p,q,r are_collinear
by A3, A5, Th3; verum