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

now :: thesis: for P being Subset of X holds
( ( 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 )

proof

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;

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

proof

set x = the Element of P;
assume A4: P in S2 ; :: thesis: P in S1
then A5: P <> {} by Def4;
then the Element of P in P ;
then reconsider x = the Element of P as Element of X ;
P = EqClass (x,S2) by A4, A5, Def6;
then P = EqClass (x,S1) by A1;
hence P in S1 by Def6; :: thesis: verum

end;

end;

hence S1 = S2 by SETFAM_1:31; :: thesis: verum