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