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;

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;

end;