for POS being OrtAfSp
for a, b being Element of POS
for a9, b9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)