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 object ; :: 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 object such that
A2: x in the carrier of T and
A3: x in the carrier of (CompactSublatt T) and
A4: y = d . x by FUNCT_2:64;
reconsider x = x as Element of T by A2;
x is compact by A3, WAYBEL_8:def 1;
then d . x is compact by A1;
hence y in the carrier of (CompactSublatt S) by A4, 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 Th63, Th65; :: thesis: verum

end;

assume A5: 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 A6: x in the carrier of (CompactSublatt T) by WAYBEL_8:def 1;
then d . x = (d | the carrier of (CompactSublatt T)) . x by FUNCT_1:49;
then d . x in the carrier of (CompactSublatt S) by A5, A6, FUNCT_2:5;
hence d . x is compact by WAYBEL_8:def 1; :: thesis: verum