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 is_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 is_collinear
let P be LINE of CLSP; :: thesis: ( p in P & q in P & r in P implies p,q,r is_collinear )
assume A1: ( p in P & q in P & r in P ) ; :: thesis: p,q,r is_collinear
consider a, b being Point of CLSP such that
A2: a <> b and
A3: P = Line a,b by Def7;
A4: ex x being Point of CLSP st
( x = p & a,b,x is_collinear ) by A1, A3;
A5: ex y being Point of CLSP st
( y = q & a,b,y is_collinear ) by A1, A3;
ex z being Point of CLSP st
( z = r & a,b,z is_collinear ) by A1, A3;
hence p,q,r is_collinear by A2, A4, A5, Th8; :: thesis: verum