let C be lattice-wise category; :: thesis: for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

for f being Morphism of a,b st f is iso holds

@ f is isomorphic

let a, b be Object of C; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds

@ f is isomorphic )

assume A1: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for f being Morphism of a,b st f is iso holds

@ f is isomorphic

let f be Morphism of a,b; :: thesis: ( f is iso implies @ f is isomorphic )

assume A2: ( f * (f ") = idm b & (f ") * f = idm a ) ; :: according to ALTCAT_3:def 5 :: thesis: @ f is isomorphic

A3: ( idm a = id (latt a) & idm b = id (latt b) ) by Th2;

( (@ f) * (@ (f ")) = f * (f ") & (@ (f ")) * (@ f) = (f ") * f ) by A1, Th3;

hence @ f is isomorphic by A2, A3, YELLOW16:15; :: thesis: verum

for f being Morphism of a,b st f is iso holds

@ f is isomorphic

let a, b be Object of C; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds

@ f is isomorphic )

assume A1: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for f being Morphism of a,b st f is iso holds

@ f is isomorphic

let f be Morphism of a,b; :: thesis: ( f is iso implies @ f is isomorphic )

assume A2: ( f * (f ") = idm b & (f ") * f = idm a ) ; :: according to ALTCAT_3:def 5 :: thesis: @ f is isomorphic

A3: ( idm a = id (latt a) & idm b = id (latt b) ) by Th2;

( (@ f) * (@ (f ")) = f * (f ") & (@ (f ")) * (@ f) = (f ") * f ) by A1, Th3;

hence @ f is isomorphic by A2, A3, YELLOW16:15; :: thesis: verum