for y, z being Element of sring4_8 st not y \ z is empty holds
ex P being finite Subset of sring4_8 st P is a_partition of y \ z
proof
let y, z be Element of sring4_8 ; :: thesis: ( not y \ z is empty implies ex P being finite Subset of sring4_8 st P is a_partition of y \ z )
assume not y \ z is empty ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of y \ z
y \ z in DIFFERENCE (sring4_8,sring4_8) by SETFAM_1:def 6;
hence ex P being finite Subset of sring4_8 st P is a_partition of y \ z by LemD; :: thesis: verum
end;
hence sring4_8 is diff-finite-partition-closed by SRINGS_1:def 2; :: thesis: verum