for X being set holds inf X c= sup X