let CLSP be proper CollSp; :: thesis: for P being LINE of CLSP ex a, b being Point of CLSP st
( a <> b & a in P & b in P )
let P be LINE of CLSP; :: thesis: ex a, b being Point of CLSP st
( a <> b & a in P & b in P )
consider a, b being Point of CLSP such that
A1: ( a <> b & P = Line (a,b) ) by Def7;
take a ; :: thesis: ex b being Point of CLSP st
( a <> b & a in P & b in P )
take b ; :: thesis: ( a <> b & a in P & b in P )
thus ( a <> b & a in P & b in P ) by A1, Th10; :: thesis: verum