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

PA is_coarser_than PB

let PA, PB be a_partition of Y; :: thesis: ( PA '>' PB implies PA is_coarser_than PB )

assume A1: PA '>' PB ; :: thesis: PA is_coarser_than PB

for x being set st x in PA holds

ex y being set st

( y in PB & y c= x )

PA is_coarser_than PB

let PA, PB be a_partition of Y; :: thesis: ( PA '>' PB implies PA is_coarser_than PB )

assume A1: PA '>' PB ; :: thesis: PA is_coarser_than PB

for x being set st x in PA holds

ex y being set st

( y in PB & y c= x )

proof

hence
PA is_coarser_than PB
by SETFAM_1:def 3; :: thesis: verum
let x be set ; :: thesis: ( x in PA implies ex y being set st

( y in PB & y c= x ) )

assume A2: x in PA ; :: thesis: ex y being set st

( y in PB & y c= x )

then A3: x <> {} by EQREL_1:def 4;

set u = the Element of x;

A4: the Element of x in x by A3;

union PB = Y by EQREL_1:def 4;

then consider y being set such that

A5: the Element of x in y and

A6: y in PB by A2, A4, TARSKI:def 4;

consider z being set such that

A7: z in PA and

A8: y c= z by A1, A6, SETFAM_1:def 2;

( x = z or x misses z ) by A2, A7, EQREL_1:def 4;

hence ex y being set st

( y in PB & y c= x ) by A3, A5, A6, A8, XBOOLE_0:3; :: thesis: verum

end;( y in PB & y c= x ) )

assume A2: x in PA ; :: thesis: ex y being set st

( y in PB & y c= x )

then A3: x <> {} by EQREL_1:def 4;

set u = the Element of x;

A4: the Element of x in x by A3;

union PB = Y by EQREL_1:def 4;

then consider y being set such that

A5: the Element of x in y and

A6: y in PB by A2, A4, TARSKI:def 4;

consider z being set such that

A7: z in PA and

A8: y c= z by A1, A6, SETFAM_1:def 2;

( x = z or x misses z ) by A2, A7, EQREL_1:def 4;

hence ex y being set st

( y in PB & y c= x ) by A3, A5, A6, A8, XBOOLE_0:3; :: thesis: verum