for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)