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