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