let S, T be complete LATTICE; 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; ( 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) )
( d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) implies d is compact-preserving )
assume A5:
d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S)
; d is compact-preserving
let x be Element of T; WAYBEL34:def 14 ( x is compact implies d . x is compact )
assume
x is compact
; 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; verum