let S, T be complete LATTICE; :: thesis: for d being sups-preserving Function of T,S st d is waybelow-preserving holds
d is compact-preserving
let d be sups-preserving Function of T,S; :: thesis: ( d is waybelow-preserving implies d is compact-preserving )
assume A1: for t, t9 being Element of T st t << t9 holds
d . t << d . t9 ; :: according to WAYBEL34:def 8 :: thesis: d is compact-preserving
let t be Element of T; :: according to WAYBEL34:def 14 :: thesis: ( t is compact implies d . t is compact )
assume t << t ; :: according to WAYBEL_3:def 2 :: thesis: d . t is compact
hence d . t << d . t by A1; :: according to WAYBEL_3:def 2 :: thesis: verum