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