for X being set
for L being non empty RelStr
for S being non empty full SubRelStr of L
for f, g being Function of X, the carrier of S
for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds
f <= g