let B be non empty subcategory of non empty semi-functional para-functional set-id-inheriting carrier-underlaid ; :: 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 holds a is LATTICE ) & ( for a, b being object of
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
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs A,B

let b be object of ; :: thesis: b is LATTICE
reconsider a = b as object of by ALTCAT_2:30;
a is LATTICE by Def4;
hence b is LATTICE ; :: thesis: verum

end;

let a, b be object of ; :: thesis: for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs A,B
reconsider a' = a, b' = b as object of by ALTCAT_2:30;
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= <^a',b'^> & <^a',b'^> c= MonFuncs A,B ) by Def4, ALTCAT_2:32;
hence <^a,b^> c= MonFuncs A,B by XBOOLE_1:1; :: thesis: verum