theorem Th2: :: MESFUNC8:2

for X being non empty set
for F being SetSequence of X
for n being Nat holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )