:: deftheorem defines times-continuous QUANTAL1:def 8 :
for IT being non empty QuantaleStr holds
( IT is times-continuous iff for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds
("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT) );