theorem Th30: :: SETLIM_1:30

for X being set
for B being SetSequence of X
for n being Element of NAT holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `