let x be non empty set ; :: thesis: ( x in sring4_8 implies ( {x} is Subset of sring4_8 & {x} is a_partition of x ) )
assume x in sring4_8 ; :: thesis: ( {x} is Subset of sring4_8 & {x} is a_partition of x )
then {x} c= sring4_8 by TARSKI:def 1;
hence ( {x} is Subset of sring4_8 & {x} is a_partition of x ) by EQREL_1:39; :: thesis: verum