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) ) )

( [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

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) )

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 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:28;

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;( 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:28;

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

( [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