for X, Y being set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y )