theorem Th7: :: WAYBEL16:7

for L being non empty reflexive transitive RelStr holds Filt L = Ids (L opp)