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