for L being non empty antisymmetric upper-bounded with_infima RelStr holds Top L is irreducible