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_{1}( Element of PARTITIONS Y) -> Element of $1 = EqClass (y,$1);

defpred S_{1}[ 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_{1}[d] )
and

A2: for d being Element of PARTITIONS Y st d in dom h holds

h /. d = H_{1}(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

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

y in c

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

defpred S

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

A2: for d being Element of PARTITIONS Y st d in dom h holds

h /. d = H

A3: G c= dom h by A1;

A4: for d being set st d in G holds

h . d in d

proof

dom h c= G
by A1;
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;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

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

A9:
for c being set st c in rng h holds
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;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

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;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

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

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 <> {} ) )

( 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;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

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 <> {} ) )

( 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;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