let S, T be complete LATTICE; :: thesis: for f being Function of S,T
for N being net of S
for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let f be Function of S,T; :: thesis: for N being net of S
for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let N be net of S; :: thesis: for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let j be Element of N; :: thesis: for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let j9 be Element of (f * N); :: thesis: ( j9 = j & f is monotone implies f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T) )
assume A1: j9 = j ; :: thesis: ( not f is monotone or f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T) )
assume A2: f is monotone ; :: thesis: f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def 8;
A5: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
A6: { ((f * N) . l) where l is Element of (f * N) : l >= j9 } c= f .: { (N . l1) where l1 is Element of N : l1 >= j }

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } or s in f .: { (N . l1) where l1 is Element of N : l1 >= j } )
assume s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ; :: thesis: s in f .: { (N . l1) where l1 is Element of N : l1 >= j }
then consider x being Element of (f * N) such that
A7: s = (f * N) . x and
A8: x >= j9 ;
reconsider x = x as Element of N by A4;
[j9,x] in the InternalRel of (f * N) by A8, ORDERS_2:def 5;
then A9: x >= j by A1, A4, ORDERS_2:def 5;
A10: s = (f * the mapping of N) . x by A7, WAYBEL_9:def 8
.= f . (N . x) by A5, FUNCT_1:13 ;
N . x in { (N . z) where z is Element of N : z >= j } by A9;
hence s in f .: { (N . l1) where l1 is Element of N : l1 >= j } by A3, A10, FUNCT_1:def 6; :: thesis: verum

end;

A11: f .: { (N . l1) where l1 is Element of N : l1 >= j } c= { ((f * N) . l) where l is Element of (f * N) : l >= j9 }

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in f .: { (N . l1) where l1 is Element of N : l1 >= j } or s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } )
assume s in f .: { (N . l1) where l1 is Element of N : l1 >= j } ; :: thesis: s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 }
then consider x being object such that
x in dom f and
A12: x in { (N . l1) where l1 is Element of N : l1 >= j } and
A13: s = f . x by FUNCT_1:def 6;
consider l2 being Element of N such that
A14: x = N . l2 and
A15: l2 >= j by A12;
reconsider l29 = l2 as Element of (f * N) by A4;
A16: s = (f * the mapping of N) . l2 by A5, A13, A14, FUNCT_1:13
.= (f * N) . l29 by WAYBEL_9:def 8 ;
[j,l2] in the InternalRel of N by A15, ORDERS_2:def 5;
then l29 >= j9 by A1, A4, ORDERS_2:def 5;
hence s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } by A16; :: thesis: verum

end;

set K = { (N . k) where k is Element of N : k >= j } ;
{ (N . k) where k is Element of N : k >= j } c= the carrier of S

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { (N . k) where k is Element of N : k >= j } or r in the carrier of S )
assume r in { (N . k) where k is Element of N : k >= j } ; :: thesis: r in the carrier of S
then ex f being Element of N st
( r = N . f & f >= j ) ;
hence r in the carrier of S ; :: thesis: verum

end;

then reconsider K = { (N . k) where k is Element of N : k >= j } as Subset of S ;
{ ((f * N) . l) where l is Element of (f * N) : l >= j9 } = f .: K by A6, A11;
hence f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T) by A2, Lm7; :: thesis: verum