let X be set ; :: thesis: for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for SM being finite Subset of S ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis: for SM being finite Subset of S ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )
let SM be finite Subset of S; :: thesis: ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )

per cases ( SM is empty or not SM is empty ) ;

suppose A1: SM is empty ; :: thesis: ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )

for Y being Element of SM holds Y = union { s where s is Element of S : ( s in {} & s c= Y ) }

proof

let Y be Element of SM; :: thesis: Y = union { s where s is Element of S : ( s in {} & s c= Y ) }
A2: Y = {} by A1, SUBSET_1:def 1;
union { s where s is Element of S : ( s in {} & s c= Y ) } c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { s where s is Element of S : ( s in {} & s c= Y ) } or x in {} )
assume x in union { s where s is Element of S : ( s in {} & s c= Y ) } ; :: thesis: x in {}
then consider y being set such that
x in y and
A3: y in { s where s is Element of S : ( s in {} & s c= Y ) } by TARSKI:def 4;
consider s being Element of S such that
y = s and
A4: s in {} and
s c= Y by A3;
thus x in {} by A4; :: thesis: verum

end;

hence Y = union { s where s is Element of S : ( s in {} & s c= Y ) } by A2; :: thesis: verum

end;

hence ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) ) by A1, ZFMISC_1:2, EQREL_1:45; :: thesis: verum

end;

suppose A5: not SM is empty ; :: thesis: ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )

consider FSM being FinSequence such that
A6: SM = rng FSM by FINSEQ_1:52;
FSM is FinSequence of S by A6, FINSEQ_1:def 4;
then consider P being finite Subset of S such that
A7: P is a_partition of Union FSM and
A8: for n being Nat st n in dom FSM holds
FSM . n = union { s where s is Element of S : ( s in P & s c= FSM . n ) } by Lem10;
for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) }

proof

let Y be Element of SM; :: thesis: Y = union { s where s is Element of S : ( s in P & s c= Y ) }
consider i being object such that
A9: i in dom FSM and
A10: Y = FSM . i by A5, A6, FUNCT_1:def 3;
thus Y c= union { s where s is Element of S : ( s in P & s c= Y ) } by A9, A10, A8; :: according to XBOOLE_0:def 10 :: thesis: union { s where s is Element of S : ( s in P & s c= Y ) } c= Y
thus union { s where s is Element of S : ( s in P & s c= Y ) } c= Y by A9, A10, A8; :: thesis: verum

end;

hence ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) ) by A6, A7; :: thesis: verum

end;

end;