theorem Th21: :: YELLOW15:24

for L being non empty RelStr holds
( [#] L is with_bottom & [#] L is with_top )