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