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