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 A3:
x in PA
;
ex y being set st
( y in PB & y c= x )
then A4:
x <> {}
by EQREL_1:def 6;
consider u being
Element of
x;
A5:
u in x
by A4;
union PB = Y
by EQREL_1:def 6;
then consider y being
set such that A7:
u in y
and A8:
y in PB
by A3, A5, TARSKI:def 4;
consider z being
set such that A9:
z in PA
and A10:
y c= z
by A1, A8, SETFAM_1:def 2;
(
x = z or
x misses z )
by A3, A9, EQREL_1:def 6;
hence
ex
y being
set st
(
y in PB &
y c= x )
by A4, A7, A8, A10, XBOOLE_0:3;
verum
end;
hence
PA is_coarser_than PB
by SETFAM_1:def 3; verum