let A be non empty finite set ; for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds
for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2
let PA1, PA2 be a_partition of A; ( PA1 is_finer_than PA2 implies for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2 )
assume A1:
PA1 is_finer_than PA2
; for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2
let p2 be Element of PA2; ex p1 being Element of PA1 st p1 c= p2
consider E1 being Equivalence_Relation of A such that
A2:
PA1 = Class E1
by EQREL_1:34;
reconsider p29 = p2 as Subset of A ;
consider E2 being Equivalence_Relation of A such that
A3:
PA2 = Class E2
by EQREL_1:34;
consider a being object such that
A4:
a in A
and
A5:
p29 = Class (E2,a)
by A3, EQREL_1:def 3;
A6:
a in Class (E1,a)
by A4, EQREL_1:20;
reconsider E1a = Class (E1,a) as Element of PA1 by A2, A4, EQREL_1:def 3;
consider p22 being set such that
A7:
p22 in PA2
and
A8:
E1a c= p22
by A1, SETFAM_1:def 2;
reconsider p229 = p22 as Subset of A by A7;
take
E1a
; E1a c= p2
ex b being object st
( b in A & p229 = Class (E2,b) )
by A3, A7, EQREL_1:def 3;
hence
E1a c= p2
by A5, A8, A6, EQREL_1:23; verum