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

proof

let y be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [y,b₁] in [:X,X:] or [y,b₁] in EqR )
let z be set ; :: 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:106;
then [z,x] in EqR by Th27;
then A3: [x,z] in EqR by Th12;
y in Class (EqR,x) by A1, A2, ZFMISC_1:106;
then [y,x] in EqR by Th27;
hence [y,z] in EqR by A3, Th13; :: thesis: verum

end;

hence EqR = nabla X by XBOOLE_0:def 10; :: thesis: verum