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 )
A1: (nabla Y) * R c= nabla Y by Th3;
(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 by A1, XBOOLE_0:def 10; :: thesis: R * (nabla Y) = nabla Y
A2: R * (nabla Y) c= nabla Y by Th3;
(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 by A2, XBOOLE_0:def 10; :: thesis: verum