let X, Y be ordinal-membered 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 in y iff f . x in 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 in y iff f . x in 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 in y iff f . x in f . y )
let x, y be set ; :: thesis: ( x in X & y in X implies ( x in y iff f . x in f . y ) )
assume A2: ( x in X & y in X ) ; :: thesis: ( 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 A1;
then ( f . x in Y & f . y in Y ) by A2, FUNCT_1:def 3;
then reconsider a = f . x, b = f . y, x = x, y = y as Ordinal by A2;
( y c= x iff b c= a ) by A1, A2, Th6;
hence ( x in y iff f . x in f . y ) by Th4; :: thesis: verum