let X be non empty set ; :: thesis: for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) holds

S1 = S2

let S1, S2 be a_partition of X; :: thesis: ( ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) implies S1 = S2 )

assume A1: for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ; :: thesis: S1 = S2

S1 = S2

let S1, S2 be a_partition of X; :: thesis: ( ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) implies S1 = S2 )

assume A1: for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ; :: thesis: S1 = S2

now :: thesis: for P being Subset of X holds

( ( P in S1 implies P in S2 ) & ( P in S2 implies P in S1 ) )

hence
S1 = S2
by SETFAM_1:31; :: thesis: verum( ( P in S1 implies P in S2 ) & ( P in S2 implies P in S1 ) )

let P be Subset of X; :: thesis: ( ( P in S1 implies P in S2 ) & ( P in S2 implies P in S1 ) )

thus ( P in S1 implies P in S2 ) :: thesis: ( P in S2 implies P in S1 )

end;thus ( P in S1 implies P in S2 ) :: thesis: ( P in S2 implies P in S1 )

proof

thus
( P in S2 implies P in S1 )
:: thesis: verum
set x = the Element of P;

assume A2: P in S1 ; :: thesis: P in S2

then A3: not P is empty by Def4;

then the Element of P in P ;

then reconsider x = the Element of P as Element of X ;

P = EqClass (x,S1) by A2, A3, Def6;

then P = EqClass (x,S2) by A1;

hence P in S2 by Def6; :: thesis: verum

end;assume A2: P in S1 ; :: thesis: P in S2

then A3: not P is empty by Def4;

then the Element of P in P ;

then reconsider x = the Element of P as Element of X ;

P = EqClass (x,S1) by A2, A3, Def6;

then P = EqClass (x,S2) by A1;

hence P in S2 by Def6; :: thesis: verum