let S, T be complete LATTICE; 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; 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; 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; 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); ( 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
; ( 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
; 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 }
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 }
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
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; verum