let Y be non empty set ; :: thesis: for R being Equivalence_Relation of Y holds

( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )

let R be Equivalence_Relation of Y; :: thesis: ( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )

(nabla Y) \/ R c= (nabla Y) * R by Th2;

then nabla Y c= (nabla Y) * R by EQREL_1:1;

hence (nabla Y) * R = nabla Y ; :: thesis: R * (nabla Y) = nabla Y

(nabla Y) \/ R c= R * (nabla Y) by Th2;

then nabla Y c= R * (nabla Y) by EQREL_1:1;

hence R * (nabla Y) = nabla Y ; :: thesis: verum

( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )

let R be Equivalence_Relation of Y; :: thesis: ( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )

(nabla Y) \/ R c= (nabla Y) * R by Th2;

then nabla Y c= (nabla Y) * R by EQREL_1:1;

hence (nabla Y) * R = nabla Y ; :: thesis: R * (nabla Y) = nabla Y

(nabla Y) \/ R c= R * (nabla Y) by Th2;

then nabla Y c= R * (nabla Y) by EQREL_1:1;

hence R * (nabla Y) = nabla Y ; :: thesis: verum