let Y be non empty set ; 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; ( PA '>' PB implies PA is_coarser_than PB )
assume A1:
PA '>' PB
; 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
let x be
set ;
( x in PA implies ex y being set st
( y in PB & y c= x ) )
assume A2:
x in PA
;
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;
verum
end;
hence
PA is_coarser_than PB
by SETFAM_1:def 3; verum