theorem Th42: :: YELLOW_2:42

for x being set
for L being non empty reflexive transitive RelStr
for I being Element of (InclPoset (Ids L)) st x in I holds
x is Element of L