theorem :: WAYBEL10:4

for L being RelStr
for S being Subset of L holds
( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds
f is monotone ) )