let X be non empty set ; :: thesis: for D being non empty a_partition of X

for p being Element of X

for A being Element of D st p in A holds

A = (proj D) . p

let D be non empty a_partition of X; :: thesis: for p being Element of X

for A being Element of D st p in A holds

A = (proj D) . p

let p be Element of X; :: thesis: for A being Element of D st p in A holds

A = (proj D) . p

let A be Element of D; :: thesis: ( p in A implies A = (proj D) . p )

assume A1: p in A ; :: thesis: A = (proj D) . p

p in (proj D) . p by Def9;

then ( (proj D) . p is Subset of X & not (proj D) . p misses A ) by A1, TARSKI:def 3, XBOOLE_0:3;

hence A = (proj D) . p by Def4; :: thesis: verum

for p being Element of X

for A being Element of D st p in A holds

A = (proj D) . p

let D be non empty a_partition of X; :: thesis: for p being Element of X

for A being Element of D st p in A holds

A = (proj D) . p

let p be Element of X; :: thesis: for A being Element of D st p in A holds

A = (proj D) . p

let A be Element of D; :: thesis: ( p in A implies A = (proj D) . p )

assume A1: p in A ; :: thesis: A = (proj D) . p

p in (proj D) . p by Def9;

then ( (proj D) . p is Subset of X & not (proj D) . p misses A ) by A1, TARSKI:def 3, XBOOLE_0:3;

hence A = (proj D) . p by Def4; :: thesis: verum