let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds
( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
let F be Function; :: thesis: ( F is_isomorphism_of R,S implies ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) ) )
assume A1: F is_isomorphism_of R,S ; :: thesis: ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
then A2: ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) by Def7;
then A3: ( rng (F " ) = dom F & dom (F " ) = rng F ) by FUNCT_1:55;
thus ( R is reflexive implies S is reflexive ) :: thesis: ( ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )

proof

assume A4: R is reflexive ; :: thesis: S is reflexive

now

let a be set ; :: thesis: ( a in field S implies [a,a] in S )
assume A5: a in field S ; :: thesis: [a,a] in S
then A6: a = F . ((F " ) . a) by A2, FUNCT_1:57;
(F " ) . a in field R by A2, A3, A5, FUNCT_1:def 5;
then [((F " ) . a),((F " ) . a)] in R by A4, Lm1;
hence [a,a] in S by A1, A6, Def7; :: thesis: verum

end;

hence S is reflexive by Lm1; :: thesis: verum

end;

thus ( R is transitive implies S is transitive ) :: thesis: ( ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )

proof

assume A7: R is transitive ; :: thesis: S is transitive

now

let a, b, c be set ; :: thesis: ( [a,b] in S & [b,c] in S implies [a,c] in S )
assume A8: ( [a,b] in S & [b,c] in S ) ; :: thesis: [a,c] in S
then A9: ( a in field S & b in field S & c in field S ) by RELAT_1:30;
then A10: ( a = F . ((F " ) . a) & b = F . ((F " ) . b) & c = F . ((F " ) . c) ) by A2, FUNCT_1:57;
( (F " ) . a in field R & (F " ) . b in field R & (F " ) . c in field R ) by A2, A3, A9, FUNCT_1:def 5;
then ( [((F " ) . a),((F " ) . b)] in R & [((F " ) . b),((F " ) . c)] in R ) by A1, A8, A10, Def7;
then [((F " ) . a),((F " ) . c)] in R by A7, Lm2;
hence [a,c] in S by A1, A10, Def7; :: thesis: verum

end;

hence S is transitive by Lm2; :: thesis: verum

end;

thus ( R is connected implies S is connected ) :: thesis: ( ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )

proof

assume A11: R is connected ; :: thesis: S is connected

now

let a, b be set ; :: thesis: ( a in field S & b in field S & a <> b & not [a,b] in S implies [b,a] in S )
assume A12: ( a in field S & b in field S & a <> b ) ; :: thesis: ( [a,b] in S or [b,a] in S )
then A13: ( a = F . ((F " ) . a) & b = F . ((F " ) . b) ) by A2, FUNCT_1:57;
then ( (F " ) . a in field R & (F " ) . b in field R & (F " ) . a <> (F " ) . b ) by A2, A3, A12, FUNCT_1:def 5;
then ( [((F " ) . a),((F " ) . b)] in R or [((F " ) . b),((F " ) . a)] in R ) by A11, Lm4;
hence ( [a,b] in S or [b,a] in S ) by A1, A13, Def7; :: thesis: verum

end;

hence S is connected by Lm4; :: thesis: verum

end;

thus ( R is antisymmetric implies S is antisymmetric ) :: thesis: ( R is well_founded implies S is well_founded )

proof

assume A14: R is antisymmetric ; :: thesis: S is antisymmetric

now

let a, b be set ; :: thesis: ( [a,b] in S & [b,a] in S implies a = b )
assume A15: ( [a,b] in S & [b,a] in S ) ; :: thesis: a = b
then A16: ( a in field S & b in field S ) by RELAT_1:30;
then A17: ( a = F . ((F " ) . a) & b = F . ((F " ) . b) ) by A2, FUNCT_1:57;
( (F " ) . a in field R & (F " ) . b in field R ) by A2, A3, A16, FUNCT_1:def 5;
then ( [((F " ) . a),((F " ) . b)] in R & [((F " ) . b),((F " ) . a)] in R ) by A1, A15, A17, Def7;
hence a = b by A14, A17, Lm3; :: thesis: verum

end;

hence S is antisymmetric by Lm3; :: thesis: verum

end;

assume A18: for Y being set st Y c= field R & Y <> {} holds
ex x being set st
( x in Y & R -Seg x misses Y ) ; :: according to WELLORD1:def 2 :: thesis: S is well_founded
let Z be set ; :: according to WELLORD1:def 2 :: thesis: ( Z c= field S & Z <> {} implies ex a being set st
( a in Z & S -Seg a misses Z ) )
assume A19: ( Z c= field S & Z <> {} ) ; :: thesis: ex a being set st
( a in Z & S -Seg a misses Z )
then A20: ( F " Z c= dom F & F " Z <> {} ) by A2, RELAT_1:167, RELAT_1:174;
then consider x being set such that
A21: ( x in F " Z & R -Seg x misses F " Z ) by A2, A18;
take F . x ; :: thesis: ( F . x in Z & S -Seg (F . x) misses Z )
thus F . x in Z by A21, FUNCT_1:def 13; :: thesis: S -Seg (F . x) misses Z
assume not S -Seg (F . x) misses Z ; :: thesis: contradiction
then consider y being set such that
A22: ( y in S -Seg (F . x) & y in Z ) by XBOOLE_0:3;
A23: ( y = F . ((F " ) . y) & (F " ) . y in dom F ) by A2, A3, A19, A22, FUNCT_1:57, FUNCT_1:def 5;
then (F " ) . y in F " Z by A22, FUNCT_1:def 13;
then not (F " ) . y in R -Seg x by A21, XBOOLE_0:3;
then A24: ( not [((F " ) . y),x] in R or (F " ) . y = x ) by Def1;
( [y,(F . x)] in S & y <> F . x ) by A22, Def1;
hence contradiction by A2, A20, A21, A23, A24; :: thesis: verum