theorem Th16: :: WAYBEL31:16

for L1 being non empty finite reflexive transitive RelStr holds Ids L1 is finite