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

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