let X, Y be set ; :: thesis: 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 )
let f be Function; :: thesis: ( f is_isomorphism_of RelIncl X, RelIncl Y implies for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y ) )
assume A1: f is_isomorphism_of RelIncl X, RelIncl Y ; :: thesis: for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y )
let x, y be set ; :: thesis: ( x in X & y in X implies ( x c= y iff f . x c= f . y ) )
assume A2: ( x in X & y in X ) ; :: thesis: ( x c= y iff f . x c= f . y )
A3: ( field (RelIncl X) = X & field (RelIncl Y) = Y ) by WELLORD2:def 1;
then ( dom f = X & rng f = Y ) by A1;
then A4: ( f . x in Y & f . y in Y ) by A2, FUNCT_1:def 3;
( x c= y iff [x,y] in RelIncl X ) by A2, WELLORD2:def 1;
then ( x c= y iff [(f . x),(f . y)] in RelIncl Y ) by A1, A2, A3;
hence ( x c= y iff f . x c= f . y ) by A4, WELLORD2:def 1; :: thesis: verum