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:19;
[z,x] in EqR by A1, EQREL_1:19;
hence Class (EqR,x) = Class (EqR,z) by A1, EQREL_1:35
.= Class (EqR,y) by A1, A3, EQREL_1:35 ;
:: thesis: verum