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

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

set x = the Element of P;
assume A2: P in S1 ; :: thesis:
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:

end;

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

set x = the Element of P;
assume A4: P in S2 ; :: thesis:
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:

end;