:: deftheorem Def7 defines LINE COLLSP:def 7 :
for CLSP being proper CollSp
for b₂ being set holds
( b₂ is LINE of CLSP iff ex a, b being Point of CLSP st
( a <> b & b₂ = Line (a,b) ) );