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

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

consider x being Element of P;
assume A2: P in S1 ; :: thesis: P in S2
then A3: not P is empty by Def6;
then x in P ;
then reconsider x = x as Element of X ;
P = EqClass x,S1 by A2, A3, Def8;
then P = EqClass x,S2 by A1;
hence P in S2 by Def8; :: thesis: verum

end;

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

proof

consider x being Element of P;
assume A4: P in S2 ; :: thesis: P in S1
then A5: P <> {} by Def6;
then x in P ;
then reconsider x = x as Element of X ;
P = EqClass x,S2 by A4, A5, Def8;
then P = EqClass x,S1 by A1;
hence P in S1 by Def8; :: thesis: verum

end;

end;

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