let C be lattice-wise with_all_isomorphisms category; :: thesis: for a, b being Object of C

for f being Morphism of a,b st @ f is isomorphic holds

f is iso

let a, b be Object of C; :: thesis: for f being Morphism of a,b st @ f is isomorphic holds

f is iso

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

assume A1: @ f is isomorphic ; :: thesis: f is iso

then consider g being monotone Function of (latt b),(latt a) such that

A2: (@ f) * g = id (latt b) and

A3: g * (@ f) = id (latt a) by YELLOW16:15;

A4: @ f in <^a,b^> by A1, Def8;

A5: g is isomorphic by A2, A3, YELLOW16:15;

then A6: g in <^b,a^> by Def8;

reconsider g = g as Morphism of b,a by A5, Def8;

A7: @ g = g by A6, Def7;

idm b = id (latt b) by Th2;

then f * g = idm b by A2, A4, A6, A7, Th3;

then A8: g is_right_inverse_of f ;

idm a = id (latt a) by Th2;

then g * f = idm a by A3, A4, A6, A7, Th3;

then A9: g is_left_inverse_of f ;

then ( f is retraction & f is coretraction ) by A8;

hence ( f * (f ") = idm b & (f ") * f = idm a ) by A4, A6, A9, A8, ALTCAT_3:def 4; :: according to ALTCAT_3:def 5 :: thesis: verum

for f being Morphism of a,b st @ f is isomorphic holds

f is iso

let a, b be Object of C; :: thesis: for f being Morphism of a,b st @ f is isomorphic holds

f is iso

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

assume A1: @ f is isomorphic ; :: thesis: f is iso

then consider g being monotone Function of (latt b),(latt a) such that

A2: (@ f) * g = id (latt b) and

A3: g * (@ f) = id (latt a) by YELLOW16:15;

A4: @ f in <^a,b^> by A1, Def8;

A5: g is isomorphic by A2, A3, YELLOW16:15;

then A6: g in <^b,a^> by Def8;

reconsider g = g as Morphism of b,a by A5, Def8;

A7: @ g = g by A6, Def7;

idm b = id (latt b) by Th2;

then f * g = idm b by A2, A4, A6, A7, Th3;

then A8: g is_right_inverse_of f ;

idm a = id (latt a) by Th2;

then g * f = idm a by A3, A4, A6, A7, Th3;

then A9: g is_left_inverse_of f ;

then ( f is retraction & f is coretraction ) by A8;

hence ( f * (f ") = idm b & (f ") * f = idm a ) by A4, A6, A9, A8, ALTCAT_3:def 4; :: according to ALTCAT_3:def 5 :: thesis: verum