let X be non empty set ; :: thesis: for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
let S1 be a_partition of X; :: thesis: for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
let x, y be Element of X; :: thesis: ( EqClass (x,S1) meets EqClass (y,S1) implies EqClass (x,S1) = EqClass (y,S1) )
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
A2: y in Class (EQR,y) by Th20;
Class (EQR,y) in S1 by A1, Def3;
then A3: Class (EQR,y) = EqClass (y,S1) by A2, Def6;
A4: x in Class (EQR,x) by Th20;
Class (EQR,x) in S1 by A1, Def3;
then A5: Class (EQR,x) = EqClass (x,S1) by A4, Def6;
assume EqClass (x,S1) meets EqClass (y,S1) ; :: thesis: EqClass (x,S1) = EqClass (y,S1)
hence EqClass (x,S1) = EqClass (y,S1) by A5, A3, Th24; :: thesis: verum