let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st T is algebraic & ( for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds

for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

let f be Function of S,T; :: thesis: ( T is algebraic & ( for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) implies for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

assume A1: T is algebraic ; :: thesis: ( ex x being Element of S ex k being Element of T st

( k in the carrier of (CompactSublatt T) & not ( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) or for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

assume A2: for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ; :: thesis: for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

let x be Element of S; :: thesis: for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

let y be Element of T; :: thesis: ( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

A10: y << f . w ; :: thesis: y << f . x

consider h being Element of T such that

A11: h in the carrier of (CompactSublatt T) and

A12: y <= h and

A13: h <= f . w by A1, A10, WAYBEL_8:7;

consider j being Element of S such that

A14: j in the carrier of (CompactSublatt S) and

A15: j <= w and

A16: h <= f . j by A2, A11, A13;

j << x by A9, A15, WAYBEL_3:2;

then j <= x by WAYBEL_3:1;

then h <= f . x by A2, A11, A14, A16;

hence y << f . x by A11, A12, WAYBEL_8:1; :: thesis: verum

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds

for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

let f be Function of S,T; :: thesis: ( T is algebraic & ( for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) implies for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

assume A1: T is algebraic ; :: thesis: ( ex x being Element of S ex k being Element of T st

( k in the carrier of (CompactSublatt T) & not ( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) or for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

assume A2: for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ; :: thesis: for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

let x be Element of S; :: thesis: for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

let y be Element of T; :: thesis: ( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

hereby :: thesis: ( ex w being Element of S st

( w << x & y << f . w ) implies y << f . x )

given w being Element of S such that A9:
w << x
and ( w << x & y << f . w ) implies y << f . x )

assume
y << f . x
; :: thesis: ex j being Element of S st

( j << x & y << f . j )

then consider w being Element of T such that

A3: w in the carrier of (CompactSublatt T) and

A4: y <= w and

A5: w <= f . x by A1, WAYBEL_8:7;

consider j being Element of S such that

A6: j in the carrier of (CompactSublatt S) and

A7: j <= x and

A8: w <= f . j by A2, A3, A5;

take j = j; :: thesis: ( j << x & y << f . j )

thus j << x by A6, A7, WAYBEL_8:1; :: thesis: y << f . j

thus y << f . j by A3, A4, A8, WAYBEL_8:1; :: thesis: verum

end;( j << x & y << f . j )

then consider w being Element of T such that

A3: w in the carrier of (CompactSublatt T) and

A4: y <= w and

A5: w <= f . x by A1, WAYBEL_8:7;

consider j being Element of S such that

A6: j in the carrier of (CompactSublatt S) and

A7: j <= x and

A8: w <= f . j by A2, A3, A5;

take j = j; :: thesis: ( j << x & y << f . j )

thus j << x by A6, A7, WAYBEL_8:1; :: thesis: y << f . j

thus y << f . j by A3, A4, A8, WAYBEL_8:1; :: thesis: verum

A10: y << f . w ; :: thesis: y << f . x

consider h being Element of T such that

A11: h in the carrier of (CompactSublatt T) and

A12: y <= h and

A13: h <= f . w by A1, A10, WAYBEL_8:7;

consider j being Element of S such that

A14: j in the carrier of (CompactSublatt S) and

A15: j <= w and

A16: h <= f . j by A2, A11, A13;

j << x by A9, A15, WAYBEL_3:2;

then j <= x by WAYBEL_3:1;

then h <= f . x by A2, A11, A14, A16;

hence y << f . x by A11, A12, WAYBEL_8:1; :: thesis: verum