for X being OrtAfPl
for a, b, c, d being Element of X
for M being Subset of X
for M9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #)
for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b