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

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