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 XFAMILY: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:42;
hence ( A = B or A misses B ) by A4, A6, A8, A9, A11, A12, RELAT_1:42; :: thesis: verum

end;

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

now :: thesis: ( not A meets B or A = B or A misses B )

assume A meets B ; :: thesis: ( A = B or A misses B )
then consider p being object such that
A14: p in A and
A15: p in B by XBOOLE_0:3;
A16: p in meet (rng h2) by A9, A11, A13, A15, A8, RELAT_1:42, SETFAM_1:def 9;
A17: p in meet (rng h1) by A4, A6, A3, A13, A14, RELAT_1:42, SETFAM_1:def 9;
for g being object st g in G holds
h1 . g = h2 . g

proof

let g be object ; :: thesis: ( g in G implies h1 . g = h2 . g )
assume A18: 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, A18, FUNCT_1:def 3;
then A19: p in h1 . g by A17, SETFAM_1:def 1;
h2 . g in rng h2 by A8, A18, FUNCT_1:def 3;
then A20: p in h2 . g by A16, SETFAM_1:def 1;
( h1 . g in g & h2 . g in g ) by A5, A10, A18;
hence h1 . g = h2 . g by A19, A20, EQREL_1:def 4, XBOOLE_0:3; :: thesis: verum

end;

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

end;

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

end;

end;

end;

A21: Y c= union X

proof

let y be object ; :: 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
A22: y in a and
A23: 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, A23;
hence y in union X by A22, TARSKI:def 4; :: thesis: verum

end;

A24: union X c= Y

proof

let a be object ; :: 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
A25: a in p and
A26: 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, A26;
hence a in Y by A25; :: thesis: verum

end;

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 by A1;
then reconsider X = X as Subset-Family of Y ;
X is a_partition of Y by A24, A2, A21, EQREL_1:def 4, XBOOLE_0:def 10;
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