let CLSP be proper CollSp; :: thesis: for P being LINE of CLSP
for x being set st x in P holds
x is Point of CLSP
let P be LINE of CLSP; :: thesis: for x being set st x in P holds
x is Point of CLSP
let x be set ; :: thesis: ( x in P implies x is Point of CLSP )
assume A1: x in P ; :: thesis: x is Point of CLSP
consider a, b being Point of CLSP such that
A2: ( a <> b & P = Line a,b ) by Def7;
ex r being Point of CLSP st
( r = x & a,b,r is_collinear ) by A1, A2;
hence x is Point of CLSP ; :: thesis: verum