let Y be non empty set ; :: thesis: for R, S being Equivalence_Relation of Y holds R \/ S c= R * S
let R, S be Equivalence_Relation of Y; :: thesis: R \/ S c= R * S
let x, y be Element of Y; :: according to RELSET_1:def 1 :: thesis: ( not [x,y] in R \/ S or [x,y] in R * S )
assume A1: [x,y] in R \/ S ; :: thesis: [x,y] in R * S
per cases ( [x,y] in R or [x,y] in S ) by A1, XBOOLE_0:def 3;
suppose A2: [x,y] in R ; :: thesis: [x,y] in R * S
[y,y] in S by EQREL_1:5;
hence [x,y] in R * S by A2, RELAT_1:def 8; :: thesis: verum
end;
suppose A3: [x,y] in S ; :: thesis: [x,y] in R * S
[x,x] in R by EQREL_1:5;
hence [x,y] in R * S by A3, RELAT_1:def 8; :: thesis: verum
end;
end;