theorem Th4: :: NECKLA_2:4

for X being set st X in fin_RelStr_sp holds
X is non empty finite strict RelStr