let S, T be complete LATTICE; :: thesis: for d being sups-preserving Function of T,S st T is algebraic & d is compact-preserving holds
d is waybelow-preserving
let d be sups-preserving Function of T,S; :: thesis: ( T is algebraic & d is compact-preserving implies d is waybelow-preserving )
assume that
A1: T is algebraic and
A2: for t being Element of T st t is compact holds
d . t is compact ; :: according to WAYBEL34:def 14 :: thesis: d is waybelow-preserving
let t, t' be Element of T; :: according to WAYBEL34:def 8 :: thesis: ( t << t' implies d . t << d . t' )
assume t << t' ; :: thesis: d . t << d . t'
then consider k being Element of T such that
A3: ( k in the carrier of (CompactSublatt T) & t <= k & k <= t' ) by A1, WAYBEL_8:7;
k is compact by A3, WAYBEL_8:def 1;
then ( d . k is compact & d is monotone ) by A2;
then ( d . k << d . k & d . t <= d . k & d . k <= d . t' ) by A3, WAYBEL_1:def 2, WAYBEL_3:def 2;
hence d . t << d . t' by WAYBEL_3:2; :: thesis: verum