theorem Th6: :: YELLOW16:7

for T being non empty RelStr
for S being non empty SubRelStr of T
for f being Function of T,S st f * (incl (S,T)) = id S holds
f is idempotent Function of T,T