let CLSP be proper CollSp; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum