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 j' being Element of (f * N) st j' = 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 >= j' } ,T
let f be Function of S,T; :: thesis: for N being net of S
for j being Element of N
for j' being Element of (f * N) st j' = 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 >= j' } ,T
let N be net of S; :: thesis: for j being Element of N
for j' being Element of (f * N) st j' = 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 >= j' } ,T
let j be Element of N; :: thesis: for j' being Element of (f * N) st j' = 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 >= j' } ,T
let j' be Element of (f * N); :: thesis: ( j' = 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 >= j' } ,T )
assume A1: j' = 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 >= j' } ,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 >= j' } ,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 >= j' } c= f .: { (N . l1) where l1 is Element of N : l1 >= j }

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { ((f * N) . l) where l is Element of (f * N) : l >= j' } 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 >= j' } ; :: 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 >= j' ;
reconsider x = x as Element of N by A4;
[j',x] in the InternalRel of (f * N) by A8, ORDERS_2:def 9;
then A9: x >= j by A1, A4, ORDERS_2:def 9;
A10: s = (f * the mapping of N) . x by A7, WAYBEL_9:def 8
.= f . (N . x) by A5, FUNCT_1:23 ;
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 12; :: 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 >= j' }

proof

let s be set ; :: 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 >= j' } )
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 >= j' }
then consider x being set 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 12;
consider l2 being Element of N such that
A14: x = N . l2 and
A15: l2 >= j by A12;
reconsider l2' = l2 as Element of (f * N) by A4;
A16: s = (f * the mapping of N) . l2 by A5, A13, A14, FUNCT_1:23
.= (f * N) . l2' by WAYBEL_9:def 8 ;
[j,l2] in the InternalRel of N by A15, ORDERS_2:def 9;
then l2' >= j' by A1, A4, ORDERS_2:def 9;
hence s in { ((f * N) . l) where l is Element of (f * N) : l >= j' } 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 set ; :: 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 >= j' } = f .: K by A6, A11, XBOOLE_0:def 10;
hence f . ("/\" { (N . k) where k is Element of N : k >= j } ,S) <= "/\" { ((f * N) . l) where l is Element of (f * N) : l >= j' } ,T by A2, Lm7; :: thesis: verum