:: deftheorem defines sring4_8 SRINGS_2:def 1 :
sring4_8 = {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};