theorem Th1: :: SETLIM_2:1

for n being Nat
for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)