let X be set ; :: thesis: for S being Subset-Family of X st S is diff-finite-partition-closed holds
S is diff-c=-finite-partition-closed
let S be Subset-Family of X; :: thesis: ( S is diff-finite-partition-closed implies S is diff-c=-finite-partition-closed )
assume A1: S is diff-finite-partition-closed ; :: thesis: S is diff-c=-finite-partition-closed
let S1, S2 be Element of S; :: according to SRINGS_1:def 3 :: thesis: ( S2 c= S1 implies ex x being finite Subset of S st x is a_partition of S1 \ S2 )
assume S2 c= S1 ; :: thesis: ex x being finite Subset of S st x 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 x being finite Subset of S st x is a_partition of S1 \ S2
( {} is finite Subset of S & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
hence ex x being finite Subset of S st x is a_partition of S1 \ S2 by A2; :: thesis: verum
end;
suppose not S1 \ S2 is empty ; :: thesis: ex x being finite Subset of S st x is a_partition of S1 \ S2
then consider x being finite Subset of S such that
A3: x is a_partition of S1 \ S2 by A1;
thus ex x being finite Subset of S st x is a_partition of S1 \ S2 by A3; :: thesis: verum
end;
end;