let X be set ; :: thesis: for x being object

for EqR being Equivalence_Relation of X st x in Class EqR holds

ex y being Element of X st x = Class (EqR,y)

let x be object ; :: thesis: for EqR being Equivalence_Relation of X st x in Class EqR holds

ex y being Element of X st x = Class (EqR,y)

let EqR be Equivalence_Relation of X; :: thesis: ( x in Class EqR implies ex y being Element of X st x = Class (EqR,y) )

assume A1: x in Class EqR ; :: thesis: ex y being Element of X st x = Class (EqR,y)

then reconsider x = x as Subset of X ;

consider y being object such that

A2: y in X and

A3: x = Class (EqR,y) by A1, Def3;

reconsider y = y as Element of X by A2;

take y ; :: thesis: x = Class (EqR,y)

thus x = Class (EqR,y) by A3; :: thesis: verum

for EqR being Equivalence_Relation of X st x in Class EqR holds

ex y being Element of X st x = Class (EqR,y)

let x be object ; :: thesis: for EqR being Equivalence_Relation of X st x in Class EqR holds

ex y being Element of X st x = Class (EqR,y)

let EqR be Equivalence_Relation of X; :: thesis: ( x in Class EqR implies ex y being Element of X st x = Class (EqR,y) )

assume A1: x in Class EqR ; :: thesis: ex y being Element of X st x = Class (EqR,y)

then reconsider x = x as Subset of X ;

consider y being object such that

A2: y in X and

A3: x = Class (EqR,y) by A1, Def3;

reconsider y = y as Element of X by A2;

take y ; :: thesis: x = Class (EqR,y)

thus x = Class (EqR,y) by A3; :: thesis: verum