let CLSP be proper CollSp; :: thesis: for a, b being Point of CLSP st a <> b holds
ex P being LINE of CLSP st
( a in P & b in P )
let a, b be Point of CLSP; :: thesis: ( a <> b implies ex P being LINE of CLSP st
( a in P & b in P ) )
assume a <> b ; :: thesis: ex P being LINE of CLSP st
( a in P & b in P )
then reconsider P = Line (a,b) as LINE of CLSP by Def7;
take P ; :: thesis: ( a in P & b in P )
thus ( a in P & b in P ) by Th10; :: thesis: verum