let X be set ; :: thesis: for EqR being Equivalence_Relation of X st ex x being object st Class (EqR,x) = X holds
EqR = nabla X
let EqR be Equivalence_Relation of X; :: thesis: ( ex x being object st Class (EqR,x) = X implies EqR = nabla X )
given x being object such that A1: Class (EqR,x) = X ; :: thesis: EqR = nabla X
[:X,X:] c= EqR

proof

let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in [:X,X:] or [y,z] in EqR )
assume A2: [y,z] in [:X,X:] ; :: thesis: [y,z] in EqR
then z in Class (EqR,x) by A1, ZFMISC_1:87;
then [z,x] in EqR by Th19;
then A3: [x,z] in EqR by Th6;
y in Class (EqR,x) by A1, A2, ZFMISC_1:87;
then [y,x] in EqR by Th19;
hence [y,z] in EqR by A3, Th7; :: thesis: verum

end;

hence EqR = nabla X ; :: thesis: verum