let B be non empty subcategory of A; :: thesis: ( B is full implies B is with_all_isomorphisms )

assume A1: B is full ; :: thesis: B is with_all_isomorphisms

let a, b be Object of B; :: according to YELLOW21:def 8 :: thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds

f in <^a,b^>

let f be Function of (latt a),(latt b); :: thesis: ( f is isomorphic implies f in <^a,b^> )

reconsider a9 = a, b9 = b as Object of A by ALTCAT_2:29;

assume f is isomorphic ; :: thesis: f in <^a,b^>

then f in <^a9,b9^> by Def8;

hence f in <^a,b^> by A1, ALTCAT_2:28; :: thesis: verum

assume A1: B is full ; :: thesis: B is with_all_isomorphisms

let a, b be Object of B; :: according to YELLOW21:def 8 :: thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds

f in <^a,b^>

let f be Function of (latt a),(latt b); :: thesis: ( f is isomorphic implies f in <^a,b^> )

reconsider a9 = a, b9 = b as Object of A by ALTCAT_2:29;

assume f is isomorphic ; :: thesis: f in <^a,b^>

then f in <^a9,b9^> by Def8;

hence f in <^a,b^> by A1, ALTCAT_2:28; :: thesis: verum