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 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 ;
then reconsider A = A as non empty set by A4, A5;
A7: now :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 take C ; :: thesis: ( ( 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] ) ) )

hereby :: thesis: 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] )
let x be LATTICE; :: thesis: ( x is Object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) )
x as_1-sorted = x by Def1;
then ( x in POSETS F1() iff ( x is strict Poset & the carrier of x in F1() ) ) by Def2;
hence ( x is Object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) by ; :: thesis: verum
end;
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; :: thesis: verum