:: deftheorem defines satisfying_des CONMETR:def 8 :
for X being OrtAfPl holds
( X is satisfying_des iff for a, a1, b, b1, c, c1 being Element of X st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );