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: { ((f * N) . l) where l is Element of (f * N) : l >= j' } = f .: { (N . l1) where l1 is Element of N : l1 >= j }

proof

A4: dom f = the carrier of S by FUNCT_2:def 1;
A5: 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;
A6: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
thus { ((f * N) . l) where l is Element of (f * N) : l >= j' } c= f .: { (N . l1) where l1 is Element of N : l1 >= j } :: according to XBOOLE_0:def 10 :: thesis: 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) . 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 & x >= j' ) ;
reconsider x = x as Element of N by A5;
[j',x] in the InternalRel of (f * N) by A7, ORDERS_2:def 9;
then A8: x >= j by A1, A5, ORDERS_2:def 9;
A9: s = (f * the mapping of N) . x by A7, WAYBEL_9:def 8
.= f . (N . x) by A6, FUNCT_1:23 ;
( N . x in dom f & N . x in { (N . z) where z is Element of N : z >= j } ) by A4, A8;
hence s in f .: { (N . l1) where l1 is Element of N : l1 >= j } by A9, FUNCT_1:def 12; :: thesis: verum

end;

thus f .: { (N . l1) where l1 is Element of N : l1 >= j } c= { ((f * N) . l) where l is Element of (f * N) : l >= j' } :: thesis: verum

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
A10: ( x in dom f & x in { (N . l1) where l1 is Element of N : l1 >= j } & s = f . x ) by FUNCT_1:def 12;
consider l2 being Element of N such that
A11: ( x = N . l2 & l2 >= j ) by A10;
reconsider l2' = l2 as Element of (f * N) by A5;
A12: s = (f * the mapping of N) . l2 by A6, A10, A11, FUNCT_1:23
.= (f * N) . l2' by WAYBEL_9:def 8 ;
[j,l2] in the InternalRel of N by A11, ORDERS_2:def 9;
then l2' >= j' by A1, A5, ORDERS_2:def 9;
hence s in { ((f * N) . l) where l is Element of (f * N) : l >= j' } by A12; :: thesis: verum

end;

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 consider f being Element of N such that
A13: ( r = N . f & f >= j ) ;
thus r in the carrier of S by A13; :: 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 A3;
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