theorem Th1: :: BINTREE2:1

for D being set
for p being FinSequence
for n being Nat st p in D * holds
p | (Seg n) in D *