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

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

hence
EqR = nabla X
; :: thesis: verum
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;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