let X, Y be ordinal-membered 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 in y iff f . x in f . y )
let f be Function; ( f is_isomorphism_of RelIncl X, RelIncl Y implies for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y ) )
assume Z0:
f is_isomorphism_of RelIncl X, RelIncl Y
; for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y )
let x, y be set ; ( x in X & y in X implies ( x in y iff f . x in f . y ) )
assume Z1:
( x in X & y in X )
; ( x in y iff f . x in f . y )
( 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
( f . x in Y & f . y in Y )
by Z1, FUNCT_1:def 3;
then reconsider a = f . x, b = f . y, x = x, y = y as Ordinal by Z1;
( y c= x iff b c= a )
by Z0, Z1, Lem1;
hence
( x in y iff f . x in f . y )
by EXCH1; verum