for POS being non empty ParOrtStr
for a, b, c, d being Element of POS
for a9, b9, c9, d9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b // c,d iff a9,b9 // c9,d9 )