let S, T be complete LATTICE; :: thesis: for d being sups-preserving Function of T,S holds
( d is compact-preserving iff d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
let d be sups-preserving Function of T,S; :: thesis: ( d is compact-preserving iff d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
thus ( d is compact-preserving implies d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ) :: thesis: ( d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) implies d is compact-preserving )

proof

assume A1: for x being Element of T st x is compact holds
d . x is compact ; :: according to WAYBEL34:def 14 :: thesis: d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S)
d .: the carrier of (CompactSublatt T) c= the carrier of (CompactSublatt S)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in d .: the carrier of (CompactSublatt T) or y in the carrier of (CompactSublatt S) )
assume y in d .: the carrier of (CompactSublatt T) ; :: thesis: y in the carrier of (CompactSublatt S)
then consider x being set such that
A2: ( x in the carrier of T & x in the carrier of (CompactSublatt T) & y = d . x ) by FUNCT_2:115;
reconsider x = x as Element of T by A2;
x is compact by A2, WAYBEL_8:def 1;
then d . x is compact by A1;
hence y in the carrier of (CompactSublatt S) by A2, WAYBEL_8:def 1; :: thesis: verum

end;

hence d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) by Th67, Th69; :: thesis: verum

end;

assume A3: d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ; :: thesis: d is compact-preserving
let x be Element of T; :: according to WAYBEL34:def 14 :: thesis: ( x is compact implies d . x is compact )
assume x is compact ; :: thesis: d . x is compact
then A4: ( x in the carrier of (CompactSublatt T) & the carrier of S <> {} ) by WAYBEL_8:def 1;
then d . x = (d | the carrier of (CompactSublatt T)) . x by FUNCT_1:72;
then d . x in the carrier of (CompactSublatt S) by A3, A4, FUNCT_2:7;
hence d . x is compact by WAYBEL_8:def 1; :: thesis: verum