let X be non empty set ; :: thesis: for D being non empty a_partition of X
for W being Element of D ex W' being Element of X st (proj D) . W' = W
let D be non empty a_partition of X; :: thesis: for W being Element of D ex W' being Element of X st (proj D) . W' = W
let W be Element of D; :: thesis: ex W' being Element of X st (proj D) . W' = W
reconsider p = W as Subset of X ;
p <> {} by EQREL_1:def 6;
then consider W' being Element of X such that
A1: W' in p by SUBSET_1:10;
take W' ; :: thesis: (proj D) . W' = W
thus (proj D) . W' = W by A1, Th29; :: thesis: verum