let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for P1, P2 being finite Subset of S
for y being non empty set st y in INTERSECTION (P1,P2) holds
ex P being finite Subset of S st P is a_partition of y
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for P1, P2 being finite Subset of S
for y being non empty set st y in INTERSECTION (P1,P2) holds
ex P being finite Subset of S st P is a_partition of y
let P1, P2 be finite Subset of S; :: thesis: for y being non empty set st y in INTERSECTION (P1,P2) holds
ex P being finite Subset of S st P is a_partition of y
let y be non empty set ; :: thesis: ( y in INTERSECTION (P1,P2) implies ex P being finite Subset of S st P is a_partition of y )
assume A1: y in INTERSECTION (P1,P2) ; :: thesis: ex P being finite Subset of S st P is a_partition of y
consider p1, p2 being set such that
A2: ( p1 in P1 & p2 in P2 & y = p1 /\ p2 ) by A1, SETFAM_1:def 5;
consider P being finite Subset of S such that
A3: P is a_partition of p1 /\ p2 by A2, Defcap;
thus ex P being finite Subset of S st P is a_partition of y by A2, A3; :: thesis: verum