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 Th43;
A2: y in Class EQR,y by Th28;
Class EQR,y in S1 by A1, Def5;
then A3: Class EQR,y = EqClass y,S1 by A2, Def8;
A4: x in Class EQR,x by Th28;
Class EQR,x in S1 by A1, Def5;
then A5: Class EQR,x = EqClass x,S1 by A4, Def8;
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, Th32; :: thesis: verum