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