let Y be non empty set ; :: thesis:
let P, Q, R be a_partition of Y; :: thesis:
assume A1: ERl R = (ERl P) * (ERl Q) ; :: thesis:
let x, y be Element of Y; :: thesis:

assume x in EqClass (y,R) ; :: thesis:
then [x,y] in ERl R by Th5;
then consider z being Element of Y such that
A2: [x,z] in ERl P and
A3: [z,y] in ERl Q by A1, RELSET_1:28;
take z = z; :: thesis:
thus x in EqClass (z,P) by A2, Th5; :: thesis:
thus z in EqClass (y,Q) by A3, Th5; :: thesis:

end;

given z being Element of Y such that A4: ( x in EqClass (z,P) & z in EqClass (y,Q) ) ; :: thesis:
( [x,z] in ERl P & [z,y] in ERl Q ) by A4, Th5;
then [x,y] in ERl R by A1, RELAT_1:def 8;
hence x in EqClass (y,R) by Th5; :: thesis: