let x, X be set ; :: 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 set such that
A2: y in X and
A3: x = Class EqR,y by A1, Def5;
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