:: deftheorem defines satisfying_3H CONAFFM:def 3 :
for X being OrtAfPl holds
( X is satisfying_3H iff for a, b, c being Element of X st not LIN a,b,c holds
ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) );