let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for y being Element of Y ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
let G be Subset of (PARTITIONS Y); :: thesis: for y being Element of Y ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
let y be Element of Y; :: thesis: ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
deffunc H₁( Element of PARTITIONS Y) -> Element of $1 = EqClass (y,$1);
defpred S₁[ set ] means $1 in G;
consider h being PartFunc of (PARTITIONS Y),(bool Y) such that
A1: for d being Element of PARTITIONS Y holds
( d in dom h iff S₁[d] ) and
A2: for d being Element of PARTITIONS Y st d in dom h holds
h /. d = H₁(d) from PARTFUN2:sch 2();
A3: G c= dom h by A1;
A4: for d being set st d in G holds
h . d in d

proof

let d be set ; :: thesis: ( d in G implies h . d in d )
assume A5: d in G ; :: thesis: h . d in d
then reconsider d = d as a_partition of Y by PARTIT1:def 3;
h /. d = h . d by A3, A5, PARTFUN1:def 6;
then h . d = EqClass (y,d) by A2, A3, A5;
hence h . d in d ; :: thesis: verum

end;

dom h c= G by A1;
then A6: dom h = G by A3, XBOOLE_0:def 10;
reconsider rr = rng h as Subset-Family of Y ;
A7: for d being Element of PARTITIONS Y st d in dom h holds
y in h . d

proof

let d be Element of PARTITIONS Y; :: thesis: ( d in dom h implies y in h . d )
assume A8: d in dom h ; :: thesis: y in h . d
then h /. d = EqClass (y,d) by A2;
then h . d = EqClass (y,d) by A8, PARTFUN1:def 6;
hence y in h . d by EQREL_1:def 6; :: thesis: verum

end;

A9: for c being set st c in rng h holds
y in c

proof

let c be set ; :: thesis: ( c in rng h implies y in c )
assume c in rng h ; :: thesis: y in c
then ex a being object st
( a in dom h & c = h . a ) by FUNCT_1:def 3;
hence y in c by A7; :: thesis: verum

end;

per cases ( rng h = {} or rng h <> {} ) ;

suppose rng h = {} ; :: thesis: ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )

then Intersect rr = Y by SETFAM_1:def 9;
hence ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) ) by A6, A4; :: thesis: verum

end;

suppose rng h <> {} ; :: thesis: ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )

then ( y in meet (rng h) & Intersect rr = meet (rng h) ) by A9, SETFAM_1:def 1, SETFAM_1:def 9;
hence ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) ) by A6, A4; :: thesis: verum

end;

end;