theorem thmIL: :: SRINGS_1:3

for X being set st X is cap-closed & X is cup-closed holds
X is Ring_of_sets