{} in sring4_8 by ENUMSET1:def 6;
hence not sring4_8 is with_non-empty_elements ; :: thesis: verum