theorem Th93: :: CLASSES4:93

for X being set holds rng (sequence_univers X) c= union_sequence_univers X