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 }

{ (N . k) where k is Element of N : k >= j } c= the carrier 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

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

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 }
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;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

proof

set K = { (N . k) where k is Element of N : k >= j } ;
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;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

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

proof

then reconsider K = { (N . k) where k is Element of N : k >= j } as Subset of S ;
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;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

{ ((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