:: deftheorem defines \/-distributive LATTICE3:def 19 :
for IT being non empty LattStr holds
( IT is \/-distributive iff for X being set
for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c );