defpred S1[ object ] means ( $1 is LATTICE & P1[$1] );
consider A being set such that
A4:
for x being object holds
( x in A iff ( x in POSETS F1() & S1[x] ) )
from XBOOLE_0:sch 1();
consider x being strict LATTICE such that
A5:
P1[x]
and
A6:
the carrier of x in F1()
by A1;
x as_1-sorted = x
by Def1;
then
x in POSETS F1()
by A6, Def2;
then reconsider A = A as non empty set by A4, A5;
A7:
now for a, b, c being LATTICE st a in A & b in A & c in A holds
for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f]let a,
b,
c be
LATTICE;
( a in A & b in A & c in A implies for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] )assume that A8:
(
a in A &
b in A )
and A9:
c in A
;
for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f]A10:
P1[
c]
by A4, A9;
(
P1[
a] &
P1[
b] )
by A4, A8;
hence
for
f being
Function of
a,
b for
g being
Function of
b,
c st
P2[
a,
b,
f] &
P2[
b,
c,
g] holds
P2[
a,
c,
g * f]
by A2, A10;
verum end;
A11:
for a being LATTICE st a in A holds
P2[a,a, id a]
by A3, A4;
A12:
for a being Element of A holds a is LATTICE
by A4;
consider C being strict lattice-wise category such that
A13:
the carrier of C = A
and
A14:
for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] )
from YELLOW21:sch 2(A12, A7, A11);
take
C
; ( ( for x being LATTICE holds
( x is Object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) )
thus
for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] )
by A14; verum