theorem :: CONMETR1:17

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