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: dom h c= G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom h or x in G )
assume x in dom h ; :: thesis: x in G
hence x in G by A1; :: thesis: verum

end;

A4: G c= dom h

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in dom h )
assume x in G ; :: thesis: x in dom h
hence x in dom h by A1; :: thesis: verum

end;

then A5: dom h = G by A3, XBOOLE_0:def 10;
A6: 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 A7: 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 A4, A7, PARTFUN1:def 8;
then h . d = EqClass y,d by A2, A4, A7;
hence h . d in d ; :: thesis: verum

end;

A8: 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 A9: d in dom h ; :: thesis: y in h . d
then h /. d = EqClass y,d by A2;
then h . d = EqClass y,d by A9, PARTFUN1:def 8;
hence y in h . d by EQREL_1:def 8; :: thesis: verum

end;

A10: 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 consider a being set such that
A11: ( a in dom h & c = h . a ) by FUNCT_1:def 5;
thus y in c by A8, A11; :: thesis: verum

end;

reconsider rr = rng h as Subset-Family of Y ;

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 10;
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 A5, A6; :: thesis: verum

end;

suppose A12: 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 A13: y in meet (rng h) by A10, SETFAM_1:def 1;
Intersect rr = meet (rng h) by A12, SETFAM_1:def 10;
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 A5, A6, A13; :: thesis: verum

end;

end;