for S, T, T1 being non empty RelStr st T is full SubRelStr of T1 holds
for f being Function of S,T
for f1 being Function of S,T1 st f1 is monotone & f = f1 holds
f is monotone