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 ( 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 ) ; :: thesis: b,c _|_ b1,c1
hence b,c _|_ b1,c1 by A1, Def4; :: thesis: verum