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