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