theorem Th55: :: WAYBEL23:55

for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set st x in rng (idsMap S) holds
x is Ideal of L