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 )
consider a, b being Point of CLSP such that
a <> b and
A1: P = Line (a,b) by Def7;
assume x in P ; :: thesis: x is Point of CLSP
then ex r being Point of CLSP st
( r = x & a,b,r are_collinear ) by A1;
hence x is Point of CLSP ; :: thesis: verum