theorem Th18: :: FINSEQ_6:18

for p being set holds p .. <*p*> = 1