let X be non empty set ; :: thesis: for P being a_partition of X
for x, y, z being set st x in P & y in P & z in x & z in y holds
x = y
let P be a_partition of X; :: thesis: for x, y, z being set st x in P & y in P & z in x & z in y holds
x = y
let x, y, z be set ; :: thesis: ( x in P & y in P & z in x & z in y implies x = y )
assume that
A1: x in P and
A2: y in P and
A3: z in x and
A4: z in y ; :: thesis: x = y
consider EqR being Equivalence_Relation of X such that
A5: P = Class EqR by EQREL_1:34;
A6: ex y9 being Element of X st y = Class (EqR,y9) by A2, A5, EQREL_1:36;
ex x9 being Element of X st x = Class (EqR,x9) by A1, A5, EQREL_1:36;
hence x = y by A3, A4, A6, Th2; :: thesis: verum