theorem Th20: :: WAYBEL17:20

for S, T being 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)