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 a' = a, b' = b as object of A by ALTCAT_2:30;
assume f is isomorphic ; :: thesis: f in <^a,b^>
then ( f in <^a',b'^> & <^a,b^> = <^a',b'^> ) by A1, Def8, ALTCAT_2:29;
hence f in <^a,b^> ; :: thesis: verum