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 6;
A3: PA is_coarser_than PB by A1, Th7;
for b being set st b in PA holds
b is_a_dependent_set_of PB

proof

let b be set ; :: thesis: ( b in PA implies b is_a_dependent_set_of PB )
assume A5: 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
A6: ( xb in PB & xb c= b ) by A3, A5, SETFAM_1:def 3;
A7: xb in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A6;
for z being set st z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } holds
z in PB

proof

let z be set ; :: 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;

then A11: { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= PB by TARSKI:def 3;
for z being set st z in b holds
z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) }

proof

let z be set ; :: thesis: ( z in b implies z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } )
assume A13: 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
A14: z in x1 and
A15: x1 in PB by A2, A5, TARSKI:def 4;
consider y1 being set such that
A16: y1 in PA and
A17: x1 c= y1 by A1, A15, SETFAM_1:def 2;
( b = y1 or b misses y1 ) by A5, A16, EQREL_1:def 6;
then x1 in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A13, A14, A15, A17, XBOOLE_0:3;
hence z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A14, TARSKI:def 4; :: thesis: verum

end;

then A20: b c= union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by TARSKI:def 3;
for z being set st z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } holds
z in b

proof

let z be set ; :: 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
A23: z in y and
A24: 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 A24;
hence z in b by A23; :: thesis: verum

end;

then union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= b by TARSKI:def 3;
then b = union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A20, XBOOLE_0:def 10;
hence b is_a_dependent_set_of PB by A7, A11, Def1; :: thesis: verum

end;

hence for b being set st b in PA holds
b is_a_dependent_set_of PB ; :: thesis: verum