let X be non empty set ; :: thesis: for EqR being Equivalence_Relation of X
for x, y, z being set st z in Class EqR,x & z in Class EqR,y holds
Class EqR,x = Class EqR,y
let EqR be Equivalence_Relation of X; :: thesis: for x, y, z being set st z in Class EqR,x & z in Class EqR,y holds
Class EqR,x = Class EqR,y
let x, y, z be set ; :: thesis: ( z in Class EqR,x & z in Class EqR,y implies Class EqR,x = Class EqR,y )
assume that
A1: z in Class EqR,x and
A2: z in Class EqR,y ; :: thesis: Class EqR,x = Class EqR,y
A3: [z,y] in EqR by A2, EQREL_1:27;
[z,x] in EqR by A1, EQREL_1:27;
hence Class EqR,x = Class EqR,z by A1, EQREL_1:44
.= Class EqR,y by A1, A3, EQREL_1:44 ;
:: thesis: verum