deffunc H₁( set ) -> set = the carrier of (c₁ as_1-sorted);
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 )
consider F being ManySortedSet of C 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;
A5: <^a,b^> c= MonFuncs (A,B) by A3;
b as_1-sorted = B by Def1;
then A6: F . b = the carrier of B by A4;
a as_1-sorted = A by Def1;
then F . a = the carrier of A by A4;
then MonFuncs (A,B) c= Funcs ((F . a),(F . b)) by A6, ORDERS_3:11;
hence <^a,b^> c= Funcs ((F . a),(F . b)) by A5; :: 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;
( idm a in <^a,a^> & <^a,a^> c= MonFuncs (S,S) ) by A3;
then consider f being Function of S,S such that
A7: idm a = f and
A8: f in Funcs ( the carrier of S, the carrier of S) and
f is monotone by ORDERS_3:def 6;
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
thus the_carrier_of a = dom (id (the_carrier_of a)) by RELAT_1:45
.= dom f by A1, A7
.= the carrier of S by A8, FUNCT_2:92 ; :: thesis: verum