theorem Th20: :: ANPROJ10:33

for D being set
for d being Element of D holds (Seg 1) --> d = <*d*>