:: deftheorem BowdenRedef defines satisfying_Bowden_inequality LATQUASI:def 12 :
for L being non empty join-commutative LattStr holds
( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) );