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;
A4: 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;
A8: 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 A9: z in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ; :: thesis: z in PB
A10: ex x8 being Subset of Y st
( x8 = z & x8 in PB & x8 c= b ) by A9;
thus z in PB by A10; :: thesis: verum

end;

A11: { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= PB by A8, TARSKI:def 3;
A12: 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 ) }
consider x1 being set such that
A14: z in x1 and
A15: x1 in PB by A2, A5, A13, 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;
A18: ( b = y1 or b misses y1 ) by A5, A16, EQREL_1:def 6;
A19: x1 in { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A13, A14, A15, A17, A18, XBOOLE_0:3;
thus z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A14, A19, TARSKI:def 4; :: thesis: verum

end;

A20: b c= union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } by A12, TARSKI:def 3;
A21: 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 A22: z in union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } ; :: thesis: z in b
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 A22, TARSKI:def 4;
A25: ex x8 being Subset of Y st
( x8 = y & x8 in PB & x8 c= b ) by A24;
thus z in b by A23, A25; :: thesis: verum

end;

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

end;

thus for b being set st b in PA holds
b is_a_dependent_set_of PB by A4; :: thesis: verum