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

for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds

B c= W ) holds

W = (proj D) " ((proj D) .: W)

let D be non empty a_partition of X; :: thesis: for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds

B c= W ) holds

W = (proj D) " ((proj D) .: W)

let W be Subset of X; :: thesis: ( ( for B being Subset of X st B in D & B meets W holds

B c= W ) implies W = (proj D) " ((proj D) .: W) )

assume A1: for B being Subset of X st B in D & B meets W holds

B c= W ; :: thesis: W = (proj D) " ((proj D) .: W)

W c= X ;

then W c= dom (proj D) by FUNCT_2:def 1;

hence W c= (proj D) " ((proj D) .: W) by FUNCT_1:76; :: according to XBOOLE_0:def 10 :: thesis: (proj D) " ((proj D) .: W) c= W

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (proj D) " ((proj D) .: W) or e in W )

assume A2: e in (proj D) " ((proj D) .: W) ; :: thesis: e in W

then reconsider d = e as Element of X ;

(proj D) . e in (proj D) .: W by A2, FUNCT_1:def 7;

then consider c being Element of X such that

A3: c in W and

A4: (proj D) . d = (proj D) . c by FUNCT_2:65;

reconsider B = (proj D) . c as Subset of X by TARSKI:def 3;

c in (proj D) . c by Def9;

then B meets W by A3, XBOOLE_0:3;

then A5: B c= W by A1;

d in B by A4, Def9;

hence e in W by A5; :: thesis: verum

for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds

B c= W ) holds

W = (proj D) " ((proj D) .: W)

let D be non empty a_partition of X; :: thesis: for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds

B c= W ) holds

W = (proj D) " ((proj D) .: W)

let W be Subset of X; :: thesis: ( ( for B being Subset of X st B in D & B meets W holds

B c= W ) implies W = (proj D) " ((proj D) .: W) )

assume A1: for B being Subset of X st B in D & B meets W holds

B c= W ; :: thesis: W = (proj D) " ((proj D) .: W)

W c= X ;

then W c= dom (proj D) by FUNCT_2:def 1;

hence W c= (proj D) " ((proj D) .: W) by FUNCT_1:76; :: according to XBOOLE_0:def 10 :: thesis: (proj D) " ((proj D) .: W) c= W

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (proj D) " ((proj D) .: W) or e in W )

assume A2: e in (proj D) " ((proj D) .: W) ; :: thesis: e in W

then reconsider d = e as Element of X ;

(proj D) . e in (proj D) .: W by A2, FUNCT_1:def 7;

then consider c being Element of X such that

A3: c in W and

A4: (proj D) . d = (proj D) . c by FUNCT_2:65;

reconsider B = (proj D) . c as Subset of X by TARSKI:def 3;

c in (proj D) . c by Def9;

then B meets W by A3, XBOOLE_0:3;

then A5: B c= W by A1;

d in B by A4, Def9;

hence e in W by A5; :: thesis: verum