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 and
A2: 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, A2, Th16; :: thesis: verum