defpred S_{1}[ object ] means ( $1 is LATTICE & P_{1}[$1] );

consider A being set such that

A4: for x being object holds

( x in A iff ( x in POSETS F_{1}() & S_{1}[x] ) )
from XBOOLE_0:sch 1();

consider x being strict LATTICE such that

A5: P_{1}[x]
and

A6: the carrier of x in F_{1}()
by A1;

x as_1-sorted = x by Def1;

then x in POSETS F_{1}()
by A6, Def2;

then reconsider A = A as non empty set by A4, A5;

P_{2}[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_{2}[ 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_{1}[x] & the carrier of x in F_{1}() ) ) ) & ( for a, b being Object of C

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{2}[ latt a, latt b,f] ) ) )

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{2}[ latt a, latt b,f] )
by A14; :: thesis: verum

consider A being set such that

A4: for x being object holds

( x in A iff ( x in POSETS F

consider x being strict LATTICE such that

A5: P

A6: the carrier of x in F

x as_1-sorted = x by Def1;

then x in POSETS F

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_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[a,c,g * f]

A11:
for a being LATTICE st a in A holds for f being Function of a,b

for g being Function of b,c st P

P

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_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[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_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[a,c,g * f]

A10: P_{1}[c]
by A4, A9;

( P_{1}[a] & P_{1}[b] )
by A4, A8;

hence for f being Function of a,b

for g being Function of b,c st P_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[a,c,g * f]
by A2, A10; :: thesis: verum

end;for g being Function of b,c st P

P

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

P

A10: P

( P

hence for f being Function of a,b

for g being Function of b,c st P

P

P

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

take C ; :: thesis: ( ( for x being LATTICE holds

( x is Object of C iff ( x is strict & P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

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_{2}[ latt a, latt b,f] )

thus
for a, b being Object of Cfor f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

let x be LATTICE; :: thesis: ( x is Object of C iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) )

x as_1-sorted = x by Def1;

then ( x in POSETS F_{1}() iff ( x is strict Poset & the carrier of x in F_{1}() ) )
by Def2;

hence ( x is Object of C iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) )
by A4, A13; :: thesis: verum

end;x as_1-sorted = x by Def1;

then ( x in POSETS F

hence ( x is Object of C iff ( x is strict & P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P