theorem ThmJ1: :: SRINGS_1:4

for X being set
for A being non empty set
for S being cap-finite-partition-closed Subset-Family of X
for P1, P2 being a_partition of A st P1 is finite Subset of S & P2 is finite Subset of S holds
ex P being a_partition of A st
( P is finite Subset of S & P '<' P1 '/\' P2 )