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: contradiction

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

let x be Element of X; :: thesis: EqClass (x,S1) = EqClass (x,S2)
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: verum

end;

hence contradiction by A3, Th38; :: thesis: verum