:: deftheorem defines satisfying_DES CONAFFM:def 1 :
for X being OrtAfPl holds
( X is satisfying_DES iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );