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
consider E1 being Equivalence_Relation of A such that
A2: PA1 = Class E1 by EQREL_1:43;
consider E2 being Equivalence_Relation of A such that
A3: PA2 = Class E2 by EQREL_1:43;
let p2 be Element of PA2; :: thesis: ex p1 being Element of PA1 st p1 c= p2
reconsider p2' = p2 as Subset of A ;
consider a being set such that
A4: ( a in A & p2' = Class E2,a ) by A3, EQREL_1:def 5;
reconsider E1a = Class E1,a as Element of PA1 by A2, A4, EQREL_1:def 5;
take E1a ; :: thesis: E1a c= p2
consider p22 being set such that
A5: ( p22 in PA2 & E1a c= p22 ) by A1, SETFAM_1:def 2;
reconsider p22' = p22 as Subset of A by A5;
consider b being set such that
A6: ( b in A & p22' = Class E2,b ) by A3, A5, EQREL_1:def 5;
a in Class E1,a by A4, EQREL_1:28;
hence E1a c= p2 by A4, A5, A6, EQREL_1:31; :: thesis: verum