let x be set ; :: thesis: ( x in DIFFERENCE (sring4_8,sring4_8) implies ex P being finite Subset of sring4_8 st P is a_partition of x )
assume x in DIFFERENCE (sring4_8,sring4_8) ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
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 then ( x in sring4_8 or x = {2,3} or x = {1,3} or x = {1,2} or x = {3,4} or x = {2,4} or x = {1,3,4} or x = {1,2,4} ) by ENUMSET1:def 5;
suppose x in sring4_8 ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by Thm98; :: thesis: verum
end;
suppose x = {2,3} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by Thm99; :: thesis: verum
end;
suppose x = {1,3} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV1; :: thesis: verum
end;
suppose x = {1,2} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV2; :: thesis: verum
end;
suppose x = {3,4} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV4; :: thesis: verum
end;
suppose x = {2,4} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV3; :: thesis: verum
end;
suppose x = {1,3,4} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV5; :: thesis: verum
end;
suppose x = {1,2,4} ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
hence ex P being finite Subset of sring4_8 st P is a_partition of x by ThmV6; :: thesis: verum
end;
end;