theorem Th10: :: WAYBEL_6:10

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