let Q be non empty Lattice-like complete QuasiNetStr ; :: thesis: ( Q is left-distributive & Q is right-distributive implies ( Q is times-continuous & Q is times-additive ) )
assume ( Q is left-distributive & Q is right-distributive ) ; :: thesis: ( Q is times-continuous & Q is times-additive )
hence ( ( for X, Y being Subset of Q st X is directed & Y is directed holds
("\/" X,Q) [*] ("\/" Y,Q) = "\/" { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q ) & ( for a, b, c being Element of Q holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) ) ) by Th5, Th6; :: according to QUANTAL1:def 7,QUANTAL1:def 8 :: thesis: verum