let R, S, T be Relation; :: thesis: ( R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic )

given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def 8 :: thesis: ( not S,T are_isomorphic or R,T are_isomorphic )

given G being Function such that A2: G is_isomorphism_of S,T ; :: according to WELLORD1:def 8 :: thesis: R,T are_isomorphic

take G * F ; :: according to WELLORD1:def 8 :: thesis: G * F is_isomorphism_of R,T

thus G * F is_isomorphism_of R,T by A1, A2, Th41; :: thesis: verum

given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def 8 :: thesis: ( not S,T are_isomorphic or R,T are_isomorphic )

given G being Function such that A2: G is_isomorphism_of S,T ; :: according to WELLORD1:def 8 :: thesis: R,T are_isomorphic

take G * F ; :: according to WELLORD1:def 8 :: thesis: G * F is_isomorphism_of R,T

thus G * F is_isomorphism_of R,T by A1, A2, Th41; :: thesis: verum