defpred S₁[ object ] means ( $1 is LATTICE & P₁[$1] );
consider A being set such that
A4: for x being object holds
( x in A iff ( x in POSETS F₁() & S₁[x] ) ) from XBOOLE_0:sch 1();
consider x being strict LATTICE such that
A5: P₁[x] and
A6: the carrier of x in F₁() by A1;
x as_1-sorted = x by Def1;
then x in POSETS F₁() by A6, Def2;
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 P₂[a,b,f] & P₂[b,c,g] holds
P₂[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 P₂[a,b,f] & P₂[b,c,g] holds
P₂[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 P₂[a,b,f] & P₂[b,c,g] holds
P₂[a,c,g * f]
A10: P₁[c] by A4, A9;
( P₁[a] & P₁[b] ) by A4, A8;
hence for f being Function of a,b
for g being Function of b,c st P₂[a,b,f] & P₂[b,c,g] holds
P₂[a,c,g * f] by A2, A10; :: thesis: verum

end;

A11: for a being LATTICE st a in A holds
P₂[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 P₂[ latt a, latt b,f] ) from YELLOW21:sch 2(A12, A7, A11);
take C ; :: thesis: ( ( for x being LATTICE holds
( x is Object of C iff ( x is strict & P₁[x] & the carrier of x in F₁() ) ) ) & ( for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₂[ 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 P₂[ latt a, latt b,f] )

let x be LATTICE; :: thesis: ( x is Object of C iff ( x is strict & P₁[x] & the carrier of x in F₁() ) )
x as_1-sorted = x by Def1;
then ( x in POSETS F₁() iff ( x is strict Poset & the carrier of x in F₁() ) ) by Def2;
hence ( x is Object of C iff ( x is strict & P₁[x] & the carrier of x in F₁() ) ) by A4, A13; :: 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 P₂[ latt a, latt b,f] ) by A14; :: thesis: verum