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

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