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