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, 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;
( 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:71
.= dom f by A1, A7, YELLOW18:def 10
.= the carrier of S by A8, FUNCT_2:169 ; :: thesis: verum