let MS be OrtAfPl; :: thesis: ( MS is Homogeneous iff MS is satisfying_ODES )
( MS is satisfying_ODES iff for o, a, a1, b, b1, c, c1 being Element of MS st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 ) by CONAFFM:def 4;
hence ( MS is Homogeneous iff MS is satisfying_ODES ) by Def7; :: thesis: verum