let x be set ; :: thesis:
assume x in DIFFERENCE (sring4_8,sring4_8) ; :: thesis:
then ( x in sring4_8 or x in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} ) by Thm50, XBOOLE_0:def 3;

per cases by ENUMSET1:def 5;

suppose x in sring4_8 ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by Thm98; :: thesis:

end;

suppose x = {2,3} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by Thm99; :: thesis:

end;

suppose x = {1,3} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV1; :: thesis:

end;

suppose x = {1,2} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV2; :: thesis:

end;

suppose x = {3,4} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV4; :: thesis:

end;

suppose x = {2,4} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV3; :: thesis:

end;

suppose x = {1,3,4} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV5; :: thesis:

end;

suppose x = {1,2,4} ; :: thesis:

hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV6; :: thesis:

end;

end;