let X be OrtAfPl; :: thesis: ( X is satisfying_ODES implies X is satisfying_AH )
assume A1: X is satisfying_ODES ; :: thesis: X is satisfying_AH
let o be Element of X; :: according to CONAFFM:def 2 :: thesis: for a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1
let a, a1, b, b1, c, c1 be Element of X; :: thesis: ( o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b implies b,c _|_ b1,c1 )
assume that
A2: o,a _|_ o,a1 and
A3: o,b _|_ o,b1 and
A4: o,c _|_ o,c1 and
A5: a,b _|_ a1,b1 and
o,a // b,c and
A6: a,c _|_ a1,c1 and
A7: not o,c // o,a and
A8: not o,a // o,b ; :: thesis: b,c _|_ b1,c1
thus b,c _|_ b1,c1 by A1, A2, A3, A4, A5, A6, A7, A8, Def4; :: thesis: verum