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