let x be set ; :: thesis: ( x in sring4_8 implies ex P being finite Subset of sring4_8 st P is a_partition of x )
assume A0: x in sring4_8 ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
per cases ( x is empty or not x is empty ) ;
suppose C0: x is empty ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
( {} is Subset of sring4_8 & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
hence ex P being finite Subset of sring4_8 st P is a_partition of x by C0; :: thesis: verum
end;
suppose not x is empty ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
then ( {x} is Subset of sring4_8 & {x} is a_partition of x ) by A0, LemmeA;
hence ex P being finite Subset of sring4_8 st P is a_partition of x ; :: thesis: verum
end;
end;