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

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, Th47; :: thesis: verum