let X be non empty set ; :: thesis: for p1, p2 being Element of X
for P being a_partition of X
for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds
p2 in A
let p1, p2 be Element of X; :: thesis: for P being a_partition of X
for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds
p2 in A
let P be a_partition of X; :: thesis: for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds
p2 in A
let A be Element of P; :: thesis: ( p1 in A & (proj P) . p1 = (proj P) . p2 implies p2 in A )
assume A1: p1 in A ; :: thesis: ( not (proj P) . p1 = (proj P) . p2 or p2 in A )
assume (proj P) . p1 = (proj P) . p2 ; :: thesis: p2 in A
then A2: (proj P) . p2 = A by A1, EQREL_1:65;
assume A3: not p2 in A ; :: thesis: contradiction
union P = X by EQREL_1:def 4;
then consider B being set such that
A4: p2 in B and
A5: B in P by TARSKI:def 4;
reconsider B = B as Element of P by A5;
A6: (proj P) . p2 = B by A4, EQREL_1:65;

per cases ( A = B or A misses B ) by EQREL_1:def 4;

suppose A = B ; :: thesis: contradiction

hence contradiction by A3, A4; :: thesis: verum

end;

suppose A misses B ; :: thesis: contradiction

hence contradiction by A2, A6; :: thesis: verum

end;

end;