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