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

A2: union {Y} = Y by ZFMISC_1:25;

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

for a being set st a in PA holds

ex b being set st

( b in {Y} & a c= b )

Y in {Y} by TARSKI:def 1;

hence Y is_a_dependent_set_of PA by A5, A9, Th6; :: thesis: verum

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

A2: union {Y} = Y by ZFMISC_1:25;

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

then A5:
{Y} is a_partition of Y
by A1, A2, EQREL_1:def 4;
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 A3: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds

( not B in {Y} or A = B or A misses B ) ) )

then A4: A = Y by TARSKI:def 1;

thus A <> {} by A3, 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 B in {Y} ; :: thesis: ( A = B or A misses B )

hence ( A = B or A misses B ) by A4, TARSKI:def 1; :: thesis: verum

end;( not B in {Y} or A = B or A misses B ) ) ) )

assume A3: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds

( not B in {Y} or A = B or A misses B ) ) )

then A4: A = Y by TARSKI:def 1;

thus A <> {} by A3, 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 B in {Y} ; :: thesis: ( A = B or A misses B )

hence ( A = B or A misses B ) by A4, TARSKI:def 1; :: thesis: verum

for a being set st a in PA holds

ex b being set st

( b in {Y} & a c= b )

proof

then A9:
{Y} '>' PA
by SETFAM_1:def 2;
let a be set ; :: thesis: ( a in PA implies ex b being set st

( b in {Y} & a c= b ) )

assume A6: a in PA ; :: thesis: ex b being set st

( b in {Y} & a c= b )

then A7: a <> {} by EQREL_1:def 4;

set x = the Element of a;

the Element of a in Y by A6, A7, TARSKI:def 3;

then consider b being set such that

the Element of a in b and

A8: b in {Y} by A2, TARSKI:def 4;

b = Y by A8, TARSKI:def 1;

hence ex b being set st

( b in {Y} & a c= b ) by A6, A8; :: thesis: verum

end;( b in {Y} & a c= b ) )

assume A6: a in PA ; :: thesis: ex b being set st

( b in {Y} & a c= b )

then A7: a <> {} by EQREL_1:def 4;

set x = the Element of a;

the Element of a in Y by A6, A7, TARSKI:def 3;

then consider b being set such that

the Element of a in b and

A8: b in {Y} by A2, TARSKI:def 4;

b = Y by A8, TARSKI:def 1;

hence ex b being set st

( b in {Y} & a c= b ) by A6, A8; :: thesis: verum

Y in {Y} by TARSKI:def 1;

hence Y is_a_dependent_set_of PA by A5, A9, Th6; :: thesis: verum