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

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)

hence
contradiction
by A3, Th38; :: thesis: verumlet 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;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