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
proof
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
proof
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;
then A7: { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= 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 ) }
proof
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;
then A13: b c= 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
proof
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;
then union { x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b ) } c= 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;
hence for b being set st b in PA holds
b is_a_dependent_set_of PB ; :: thesis: verum