:: deftheorem defines satisfying_DES PAPDESAF:def 6 :
for OAS being OAffinSpace holds
( OAS is satisfying_DES iff for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );