let A be non empty finite set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2
let p2 be Element of PA2; :: thesis: 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 ; :: thesis: 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; :: thesis: verum