theorem Th53: :: WAYBEL23:53

for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds
( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )