theorem Th1: :: WAYBEL19:1

for LL being non empty RelStr ex T being correct strict TopAugmentation of LL st T is lower