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