let C be Category; :: thesis: for a, b being Object of C st a,b are_isomorphic holds
b,a are_isomorphic
let a, b be Object of C; :: thesis: ( a,b are_isomorphic implies b,a are_isomorphic )
assume A1: Hom (a,b) <> {} ; :: according to CAT_1:def 14 :: thesis: ( for f being Morphism of a,b holds not f is invertible or b,a are_isomorphic )
given f being Morphism of a,b such that A2: f is invertible ; :: thesis: b,a are_isomorphic
thus A3: Hom (b,a) <> {} by A1, A2, Th70; :: according to CAT_1:def 14 :: thesis: ex f being Morphism of b,a st f is invertible
consider g being Morphism of b,a such that
A4: ( f * g = id b & g * f = id a ) by A1, A2, Th70;
take g ; :: thesis: g is invertible
thus g is invertible by A1, A3, A4, Th70; :: thesis: verum