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

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

take F " ; :: according to WELLORD1:def 8 :: thesis: F " is_isomorphism_of S,R

thus F " is_isomorphism_of S,R by A1, Th39; :: thesis: verum

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

take F " ; :: according to WELLORD1:def 8 :: thesis: F " is_isomorphism_of S,R

thus F " is_isomorphism_of S,R by A1, Th39; :: thesis: verum