let x be set ; ( 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)
; 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;