theorem Th13: :: YELLOW14:13

for L being RelStr st L is empty holds
L is bounded