let S, T be complete LATTICE; :: thesis: ( T is algebraic implies for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ) )
assume A1: T is algebraic ; :: thesis: for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
A2: T is continuous by A1;
let g be infs-preserving Function of S,T; :: thesis: ( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )

hereby :: thesis: ( (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) implies g is directed-sups-preserving )

assume g is directed-sups-preserving ; :: thesis: (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S)
then LowerAdj g is waybelow-preserving by Th24;
then LowerAdj g is compact-preserving by Th60;
hence (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) by Th70; :: thesis: verum

end;

assume (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ; :: thesis: g is directed-sups-preserving
then LowerAdj g is compact-preserving by Th70;
then LowerAdj g is waybelow-preserving by A1, Th61;
hence g is directed-sups-preserving by A2, Th25; :: thesis: verum