let Y be non empty set ; :: thesis: for PA being a_partition of Y holds Y is_a_dependent_set_of PA
let PA be a_partition of Y; :: thesis: Y is_a_dependent_set_of PA
A1: {Y} is Subset-Family of Y by ZFMISC_1:80;
A2: union {Y} = Y by ZFMISC_1:31;
A3: for A being Subset of Y st A in {Y} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )

proof

let A be Subset of Y; :: thesis: ( A in {Y} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) ) )
assume A4: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
A5: A = Y by A4, TARSKI:def 1;
thus A <> {} by A4, TARSKI:def 1; :: thesis: for B being Subset of Y holds
( not B in {Y} or A = B or A misses B )
let B be Subset of Y; :: thesis: ( not B in {Y} or A = B or A misses B )
assume A6: B in {Y} ; :: thesis: ( A = B or A misses B )
thus ( A = B or A misses B ) by A5, A6, TARSKI:def 1; :: thesis: verum

end;

A7: {Y} is a_partition of Y by A1, A2, A3, EQREL_1:def 6;
A8: for a being set st a in PA holds
ex b being set st
( b in {Y} & a c= b )

proof

let a be set ; :: thesis: ( a in PA implies ex b being set st
( b in {Y} & a c= b ) )
assume A9: a in PA ; :: thesis: ex b being set st
( b in {Y} & a c= b )
A10: a <> {} by A9, EQREL_1:def 6;
consider x being Element of a;
A11: x in Y by A9, A10, TARSKI:def 3;
consider b being set such that
x in b and
A12: b in {Y} by A2, A11, TARSKI:def 4;
A13: b = Y by A12, TARSKI:def 1;
thus ex b being set st
( b in {Y} & a c= b ) by A9, A12, A13; :: thesis: verum

end;

A14: {Y} '>' PA by A8, SETFAM_1:def 2;
A15: Y in {Y} by TARSKI:def 1;
thus Y is_a_dependent_set_of PA by A7, A14, A15, Th8; :: thesis: verum