theorem Th30: :: ABCMIZ_A:30

for i being Nat ex l being quasi-loci st len l = i