theorem Th4: :: WAYBEL13:4

for L being non empty reflexive transitive with_suprema RelStr holds the carrier of L is Ideal of L