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) ) )

<^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

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 a, b be Object of B; :: thesis: for A, B being LATTICE st A = a & B = b holds 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;reconsider a = b as Object of A by ALTCAT_2:29;

a is LATTICE by Def4;

hence b is LATTICE ; :: thesis: verum

<^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