let x be set ; :: thesis: ( x in INTERSECTION (sring4_8,sring4_8) implies ex P being finite Subset of sring4_8 st P is a_partition of x )
assume x in INTERSECTION (sring4_8,sring4_8) ; :: thesis: ex P being finite Subset of sring4_8 st P is a_partition of x
then H2: ( x in sring4_8 or x in {{2,3}} ) by LemAA, Thm1, XBOOLE_0:def 3;
( x = {2,3} implies ex P being finite Subset of sring4_8 st P is a_partition of x ) by Thm99;
hence ex P being finite Subset of sring4_8 st P is a_partition of x by H2, TARSKI:def 1, Thm98; :: thesis: verum