defpred S₁[ set ] means 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 ) & $1 = Intersect F & $1 <> {} );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool Y & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
( x in X iff 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 <> {} ) ) ) )
A2: union X = Y

proof

A3: union X c= Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in union X or a in Y )
assume a in union X ; :: thesis: a in Y
then consider p being set such that
A4: ( a in p & p in X ) by TARSKI:def 4;
consider h being Function, F being Subset-Family of Y such that
A5: ( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & p = Intersect F & p <> {} ) by A1, A4;
thus a in Y by A4, A5; :: thesis: verum

end;

Y c= union X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in union X )
assume y in Y ; :: thesis: y in union X
then reconsider y = y as Element of Y ;
consider a being Subset of Y such that
A6: ( y in a & 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 ) & a = Intersect F & a <> {} ) ) by Th1;
consider h being Function, F being Subset-Family of Y such that
A7: ( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & a = Intersect F & a <> {} ) by A6;
a in X by A1, A7;
hence y in union X by A6, TARSKI:def 4; :: thesis: verum

end;

hence union X = Y by A3, XBOOLE_0:def 10; :: thesis: verum

end;

A8: for A being Subset of Y st A in X holds
( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )

proof

let A be Subset of Y; :: thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) ) )
assume A in X ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
then consider h1 being Function, F1 being Subset-Family of Y such that
A9: ( dom h1 = G & rng h1 = F1 & ( for d being set st d in G holds
h1 . d in d ) & A = Intersect F1 & A <> {} ) by A1;
thus A <> {} by A9; :: thesis: for B being Subset of Y holds
( not B in X or A = B or A misses B )
let B be Subset of Y; :: thesis: ( not B in X or A = B or A misses B )
assume B in X ; :: thesis: ( A = B or A misses B )
then consider h2 being Function, F2 being Subset-Family of Y such that
A10: ( dom h2 = G & rng h2 = F2 & ( for d being set st d in G holds
h2 . d in d ) & B = Intersect F2 & B <> {} ) by A1;

per cases ( G = {} or G <> {} ) ;

suppose G = {} ; :: thesis: ( A = B or A misses B )

then ( rng h1 = {} & rng h2 = {} ) by A9, A10, RELAT_1:65;
hence ( A = B or A misses B ) by A9, A10; :: thesis: verum

end;

suppose G <> {} ; :: thesis: ( A = B or A misses B )

then A11: ( rng h1 <> {} & rng h2 <> {} ) by A9, A10, RELAT_1:65;

now

assume A meets B ; :: thesis: ( A = B or A misses B )
then consider p being set such that
A12: ( p in A & p in B ) by XBOOLE_0:3;
A13: p in meet (rng h1) by A9, A11, A12, SETFAM_1:def 10;
A14: p in meet (rng h2) by A10, A11, A12, SETFAM_1:def 10;
for g being set st g in G holds
h1 . g = h2 . g

proof

let g be set ; :: thesis: ( g in G implies h1 . g = h2 . g )
assume A15: g in G ; :: thesis: h1 . g = h2 . g
then reconsider g = g as a_partition of Y by PARTIT1:def 3;
A16: h1 . g in g by A9, A15;
A17: h2 . g in g by A10, A15;
A18: h1 . g in rng h1 by A9, A15, FUNCT_1:def 5;
A19: h2 . g in rng h2 by A10, A15, FUNCT_1:def 5;
A20: p in h1 . g by A13, A18, SETFAM_1:def 1;
A21: p in h2 . g by A14, A19, SETFAM_1:def 1;
( h1 . g = h2 . g or h1 . g misses h2 . g ) by A16, A17, EQREL_1:def 6;
hence h1 . g = h2 . g by A20, A21, XBOOLE_0:3; :: thesis: verum

end;

hence ( A = B or A misses B ) by A9, A10, FUNCT_1:9; :: thesis: verum

end;

hence ( A = B or A misses B ) ; :: thesis: verum

end;

end;

end;

X c= bool Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in bool Y )
assume a in X ; :: thesis: a in bool Y
then consider h being Function, F being Subset-Family of Y such that
A22: ( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & a = Intersect F & a <> {} ) by A1;
thus a in bool Y by A22; :: thesis: verum

end;

then reconsider X = X as Subset-Family of Y ;
X is a_partition of Y by A2, A8, EQREL_1:def 6;
hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
( x in X iff 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 A1; :: thesis: verum