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 )