:: deftheorem defines /\-distributive LATTICE3:def 20 :
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_greater_than a & ( for d being Element of IT st X is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds
d [= c ) holds
c [= b "\/" a );