theorem Th9: :: PAPDESAF:9

for OAP being OAffinSpace st OAP is satisfying_DES_1 holds
Lambda OAP is Desarguesian