let B be non empty subcategory of A; :: thesis: B is lattice-wise
thus ( B is semi-functional & B is set-id-inheriting ) ; :: according to YELLOW21:def 4 :: thesis: ( ( for a being Object of B holds a is LATTICE ) & ( for a, b being Object of B
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) )
hereby :: thesis: for a, b being Object of B
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B)
let b be Object of B; :: thesis: b is LATTICE
reconsider a = b as Object of A by ALTCAT_2:29;
a is LATTICE by Def4;
hence b is LATTICE ; :: thesis: verum
end;
let a, b be Object of B; :: thesis: for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B)
reconsider a9 = a, b9 = b as Object of A by ALTCAT_2:29;
let A, B be LATTICE; :: thesis: ( A = a & B = b implies <^a,b^> c= MonFuncs (A,B) )
assume ( A = a & B = b ) ; :: thesis: <^a,b^> c= MonFuncs (A,B)
then ( <^a,b^> c= <^a9,b9^> & <^a9,b9^> c= MonFuncs (A,B) ) by Def4, ALTCAT_2:31;
hence <^a,b^> c= MonFuncs (A,B) ; :: thesis: verum