let Y be non empty set ; :: thesis: for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds
for x, y being Element of Y holds
( x in EqClass y,R iff ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q ) )
let P, Q, R be a_partition of Y; :: thesis: ( ERl R = (ERl P) * (ERl Q) implies for x, y being Element of Y holds
( x in EqClass y,R iff ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q ) ) )
assume A1: ERl R = (ERl P) * (ERl Q) ; :: thesis: for x, y being Element of Y holds
( x in EqClass y,R iff ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q ) )
let x, y be Element of Y; :: thesis: ( x in EqClass y,R iff ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q ) )

hereby :: thesis: ( ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q ) implies x in EqClass y,R )

assume x in EqClass y,R ; :: thesis: ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q )
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:51;
take z = z; :: thesis: ( x in EqClass z,P & z in EqClass y,Q )
thus x in EqClass z,P by A2, Th5; :: thesis: z in EqClass y,Q
thus z in EqClass y,Q by A3, Th5; :: thesis: verum

end;

given z being Element of Y such that A4: ( x in EqClass z,P & z in EqClass y,Q ) ; :: thesis: x in EqClass y,R
( [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: verum