for X being OrtAfPl st AffinStruct(# the carrier of X, the CONGR of X #) is translational holds
X is satisfying_des