let C be category; :: thesis: ( C is lattice-wise implies ( C is concrete & C is carrier-underlaid ) )
assume that
A1: ( C is semi-functional & C is set-id-inheriting ) and
A2: for a being object of C holds a is LATTICE and
A3: for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs A,B ; :: according to YELLOW21:def 4 :: thesis: ( C is concrete & C is carrier-underlaid )
deffunc H₁( set ) -> set = the carrier of (c₁ as_1-sorted );
consider F being ManySortedSet of such that
A4: for i being Element of C holds F . i = H₁(i) from PBOOLE:sch 5();
C is para-functional

proof

take F ; :: according to YELLOW18:def 7 :: thesis: for b₁, b₂ being Element of the carrier of C holds <^b₁,b₂^> c= Funcs (F . b₁),(F . b₂)
let a, b be object of C; :: thesis: <^a,b^> c= Funcs (F . a),(F . b)
reconsider A = a, B = b as LATTICE by A2;
( a as_1-sorted = A & b as_1-sorted = B ) by Def1;
then ( F . a = the carrier of A & F . b = the carrier of B ) by A4;
then ( <^a,b^> c= MonFuncs A,B & MonFuncs A,B c= Funcs (F . a),(F . b) ) by A3, ORDERS_3:11;
hence <^a,b^> c= Funcs (F . a),(F . b) by XBOOLE_1:1; :: thesis: verum

end;

hence C is concrete by A1; :: thesis: C is carrier-underlaid
let a be object of C; :: according to YELLOW21:def 3 :: thesis: ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S )
reconsider S = a as LATTICE by A2;
take S ; :: thesis: ( a = S & the_carrier_of a = the carrier of S )
thus a = S ; :: thesis: the_carrier_of a = the carrier of S
( idm a in <^a,a^> & <^a,a^> c= MonFuncs S,S ) by A3;
then consider f being Function of S,S such that
A5: idm a = f and
A6: f in Funcs the carrier of S,the carrier of S and
f is monotone by ORDERS_3:def 6;
thus the_carrier_of a = dom (id (the_carrier_of a)) by RELAT_1:71
.= dom f by A1, A5, YELLOW18:def 10
.= the carrier of S by A6, FUNCT_2:169 ; :: thesis: verum