let X be non empty set ; 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; 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; 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; ( p1 in A & (proj P) . p1 = (proj P) . p2 implies p2 in A )
assume A1:
p1 in A
; ( not (proj P) . p1 = (proj P) . p2 or p2 in A )
assume
(proj P) . p1 = (proj P) . p2
; p2 in A
then A2:
(proj P) . p2 = A
by A1, EQREL_1:65;
assume A3:
not p2 in A
; 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;