let X be set ; :: thesis: for S being Subset-Family of X st ( for A, B being Element of S st not A \ B is empty holds
ex P being finite Subset of S st P is a_partition of A \ B ) holds
for A, B being Element of S ex P being finite Subset of S st P is a_partition of A \ B
let S be Subset-Family of X; :: thesis: ( ( for A, B being Element of S st not A \ B is empty holds
ex P being finite Subset of S st P is a_partition of A \ B ) implies for A, B being Element of S ex P being finite Subset of S st P is a_partition of A \ B )
assume A1: for A, B being Element of S st not A \ B is empty holds
ex P being finite Subset of S st P is a_partition of A \ B ; :: thesis: for A, B being Element of S ex P being finite Subset of S st P is a_partition of A \ B
let S1, S2 be Element of S; :: thesis: ex P being finite Subset of S st P is a_partition of S1 \ S2

per cases ( S1 \ S2 is empty or not S1 \ S2 is empty ) ;

suppose A2: S1 \ S2 is empty ; :: thesis: ex P being finite Subset of S st P is a_partition of S1 \ S2

( {} is finite Subset of S & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
hence ex P being finite Subset of S st P is a_partition of S1 \ S2 by A2; :: thesis: verum

end;

suppose not S1 \ S2 is empty ; :: thesis: ex P being finite Subset of S st P is a_partition of S1 \ S2

hence ex P being finite Subset of S st P is a_partition of S1 \ S2 by A1; :: thesis: verum

end;

end;