defpred S₁[ set ] means ( $1 is LATTICE & P₁[$1] );
consider A being set such that
A4: for x being set 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

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: now

let a be LATTICE; :: thesis: ( a in A implies P₂[a,a, id a] )
assume a in A ; :: thesis: P₂[a,a, id a]
then P₁[a] by A4;
hence P₂[a,a, id a] by A3; :: thesis: verum

end;

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