given S1, S2 being a_partition of X such that A1: for x being Element of X holds EqClass (x,S1) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } and
A2: for x being Element of X holds EqClass (x,S2) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } and
A3: not S1 = S2 ; :: thesis:

let x be Element of X; :: thesis:
EqClass (x,S1) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by A1;
hence EqClass (x,S1) = EqClass (x,S2) by A2; :: thesis:

end;