theorem :: CONMETR1:15

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