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