theorem Th41: :: YELLOW_2:41

for x being set
for L being non empty reflexive transitive RelStr holds
( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )