let X be set ; 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; 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; 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 ; ( 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)
; 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; verum