let z be Complex; :: thesis: for X, Y being complex-membered set holds (multRel (X,z)) \/ (multRel (Y,z)) c= multRel ((X \/ Y),z)
let X, Y be complex-membered set ; :: thesis: (multRel (X,z)) \/ (multRel (Y,z)) c= multRel ((X \/ Y),z)
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then ( multRel (X,z) c= multRel ((X \/ Y),z) & multRel (Y,z) c= multRel ((X \/ Y),z) ) by Th47;
hence (multRel (X,z)) \/ (multRel (Y,z)) c= multRel ((X \/ Y),z) by XBOOLE_1:8; :: thesis: verum