let X1, X2, Y1, Y2 be set ; :: thesis: ( X1 c= X2 & Y1 c= Y2 implies X1 ++ Y1 c= X2 ++ Y2 )
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis: X1 ++ Y1 c= X2 ++ Y2
X2 = X1 \/ (X2 \ X1) by A1, XBOOLE_1:45;
then X2 ++ Y1 = (X1 ++ Y1) \/ ((X2 \ X1) ++ Y1) by SURREALR:33;
then A2: X1 ++ Y1 c= X2 ++ Y1 by XBOOLE_1:7;
Y2 = Y1 \/ (Y2 \ Y1) by A1, XBOOLE_1:45;
then X2 ++ Y2 = (X2 ++ Y1) \/ (X2 ++ (Y2 \ Y1)) by SURREALR:33;
then X2 ++ Y1 c= X2 ++ Y2 by XBOOLE_1:7;
hence X1 ++ Y1 c= X2 ++ Y2 by A2; :: thesis: verum