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 Z0: 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 Z1: ( x in X & y in X ) ; :: thesis: ( x c= y iff f . x c= f . y )
A1: ( field (RelIncl X) = X & field (RelIncl Y) = Y ) by WELLORD2:def 1;
then ( dom f = X & rng f = Y ) by Z0, WELLORD1:def 7;
then A2: ( f . x in Y & f . y in Y ) by Z1, FUNCT_1:def 3;
( x c= y iff [x,y] in RelIncl X ) by Z1, WELLORD2:def 1;
then ( x c= y iff [(f . x),(f . y)] in RelIncl Y ) by Z0, Z1, A1, WELLORD1:def 7;
hence ( x c= y iff f . x c= f . y ) by A2, WELLORD2:def 1; :: thesis: verum