:: deftheorem Def5 defines right-distributive QUANTAL1:def 5 :
for IT being non empty QuantaleStr holds
( IT is right-distributive iff for a being Element of IT
for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT) );