theorem Th5: :: DICKSON:6

for L being RelStr
for Y, a being set holds
( ( the InternalRel of L -Seg a misses Y & a in Y ) iff a is_minimal_wrt Y, the InternalRel of L )