let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y st PA '>' PB holds

for b being set st b in PA holds

b is_a_dependent_set_of PB

let PA, PB be a_partition of Y; :: thesis: ( PA '>' PB implies for b being set st b in PA holds

b is_a_dependent_set_of PB )

assume A1: PA '>' PB ; :: thesis: for b being set st b in PA holds

b is_a_dependent_set_of PB

A2: union PB = Y by EQREL_1:def 4;

A3: PA is_coarser_than PB by A1, Th5;

for b being set st b in PA holds

b is_a_dependent_set_of PB

b is_a_dependent_set_of PB ; :: thesis: verum

for b being set st b in PA holds

b is_a_dependent_set_of PB

let PA, PB be a_partition of Y; :: thesis: ( PA '>' PB implies for b being set st b in PA holds

b is_a_dependent_set_of PB )

assume A1: PA '>' PB ; :: thesis: for b being set st b in PA holds

b is_a_dependent_set_of PB

A2: union PB = Y by EQREL_1:def 4;

A3: PA is_coarser_than PB by A1, Th5;

for b being set st b in PA holds

b is_a_dependent_set_of PB

proof

hence
for b being set st b in PA holds
let b be set ; :: thesis: ( b in PA implies b is_a_dependent_set_of PB )

assume A4: b in PA ; :: thesis: b is_a_dependent_set_of PB

set B0 = { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ;

consider xb being set such that

A5: ( xb in PB & xb c= b ) by A3, A4, SETFAM_1:def 3;

A6: xb in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A5;

for z being object st z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } holds

z in PB

for z being object st z in b holds

z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) }

for z being object st z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } holds

z in b

then b = union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A13, XBOOLE_0:def 10;

hence b is_a_dependent_set_of PB by A6, A7; :: thesis: verum

end;assume A4: b in PA ; :: thesis: b is_a_dependent_set_of PB

set B0 = { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ;

consider xb being set such that

A5: ( xb in PB & xb c= b ) by A3, A4, SETFAM_1:def 3;

A6: xb in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A5;

for z being object st z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } holds

z in PB

proof

then A7:
{ x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= PB
;
let z be object ; :: thesis: ( z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } implies z in PB )

assume z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ; :: thesis: z in PB

then ex x8 being Subset of Y st

( x8 = z & x8 in PB & x8 c= b ) ;

hence z in PB ; :: thesis: verum

end;assume z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ; :: thesis: z in PB

then ex x8 being Subset of Y st

( x8 = z & x8 in PB & x8 c= b ) ;

hence z in PB ; :: thesis: verum

for z being object st z in b holds

z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) }

proof

then A13:
b c= union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) }
;
let z be object ; :: thesis: ( z in b implies z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } )

assume A8: z in b ; :: thesis: z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) }

then consider x1 being set such that

A9: z in x1 and

A10: x1 in PB by A2, A4, TARSKI:def 4;

consider y1 being set such that

A11: y1 in PA and

A12: x1 c= y1 by A1, A10, SETFAM_1:def 2;

( b = y1 or b misses y1 ) by A4, A11, EQREL_1:def 4;

then x1 in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A8, A9, A10, A12, XBOOLE_0:3;

hence z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A9, TARSKI:def 4; :: thesis: verum

end;assume A8: z in b ; :: thesis: z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) }

then consider x1 being set such that

A9: z in x1 and

A10: x1 in PB by A2, A4, TARSKI:def 4;

consider y1 being set such that

A11: y1 in PA and

A12: x1 c= y1 by A1, A10, SETFAM_1:def 2;

( b = y1 or b misses y1 ) by A4, A11, EQREL_1:def 4;

then x1 in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A8, A9, A10, A12, XBOOLE_0:3;

hence z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A9, TARSKI:def 4; :: thesis: verum

for z being object st z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } holds

z in b

proof

then
union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= b
;
let z be object ; :: thesis: ( z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } implies z in b )

assume z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ; :: thesis: z in b

then consider y being set such that

A14: z in y and

A15: y in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by TARSKI:def 4;

ex x8 being Subset of Y st

( x8 = y & x8 in PB & x8 c= b ) by A15;

hence z in b by A14; :: thesis: verum

end;assume z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ; :: thesis: z in b

then consider y being set such that

A14: z in y and

A15: y in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by TARSKI:def 4;

ex x8 being Subset of Y st

( x8 = y & x8 in PB & x8 c= b ) by A15;

hence z in b by A14; :: thesis: verum

then b = union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A13, XBOOLE_0:def 10;

hence b is_a_dependent_set_of PB by A6, A7; :: thesis: verum

b is_a_dependent_set_of PB ; :: thesis: verum