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();
A2: 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
A3: dom h1 = G and
A4: rng h1 = F1 and
A5: for d being set st d in G holds
h1 . d in d and
A6: A = Intersect F1 and
A7: A <> {} by A1;
thus A <> {} by A7; :: 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
A8: dom h2 = G and
A9: rng h2 = F2 and
A10: for d being set st d in G holds
h2 . d in d and
A11: B = Intersect F2 and
B <> {} by A1;

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

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

then rng h1 = {} by A3, RELAT_1:65;
hence ( A = B or A misses B ) by A4, A6, A8, A9, A11, A12, RELAT_1:65; :: thesis: verum

end;

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

then A14: rng h2 <> {} by A8, RELAT_1:65;
A15: rng h1 <> {} by A3, A13, RELAT_1:65;

now

assume A meets B ; :: thesis: ( A = B or A misses B )
then consider p being set such that
A16: p in A and
A17: p in B by XBOOLE_0:3;
A18: p in meet (rng h2) by A9, A11, A14, A17, SETFAM_1:def 10;
A19: p in meet (rng h1) by A4, A6, A15, A16, 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 A20: g in G ; :: thesis: h1 . g = h2 . g
then reconsider g = g as a_partition of Y by PARTIT1:def 3;
h1 . g in rng h1 by A3, A20, FUNCT_1:def 5;
then A21: p in h1 . g by A19, SETFAM_1:def 1;
h2 . g in rng h2 by A8, A20, FUNCT_1:def 5;
then A22: p in h2 . g by A18, SETFAM_1:def 1;
( h1 . g in g & h2 . g in g ) by A5, A10, A20;
then ( h1 . g = h2 . g or h1 . g misses h2 . g ) by EQREL_1:def 6;
hence h1 . g = h2 . g by A21, A22, XBOOLE_0:3; :: thesis: verum

end;

hence ( A = B or A misses B ) by A3, A4, A6, A8, A9, A11, FUNCT_1:9; :: thesis: verum

end;

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

end;

end;

end;

A23: 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
A24: y in a and
A25: 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;
a in X by A1, A25;
hence y in union X by A24, TARSKI:def 4; :: thesis: verum

end;

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
A26: a in p and
A27: p in X by TARSKI:def 4;
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 ) & p = Intersect F & p <> {} ) by A1, A27;
hence a in Y by A26; :: thesis: verum

end;

then A28: union X = Y by A23, XBOOLE_0:def 10;
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 <> {} ) ) ) )
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
hence a in bool Y by A1; :: thesis: verum

end;

then reconsider X = X as Subset-Family of Y ;
X is a_partition of Y by A28, A2, 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