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, t9 be Element of T; :: according to WAYBEL34:def 8 :: thesis: ( t << t9 implies d . t << d . t9 )
assume t << t9 ; :: thesis: d . t << d . t9
then consider k being Element of T such that
A3: k in the carrier of (CompactSublatt T) and
A4: t <= k and
A5: k <= t9 by A1, WAYBEL_8:7;
k is compact by A3, WAYBEL_8:def 1;
then d . k is compact by A2;
then A6: d . k << d . k ;
A7: d . t <= d . k by A4, WAYBEL_1:def 2;
d . k <= d . t9 by A5, WAYBEL_1:def 2;
hence d . t << d . t9 by A6, A7, WAYBEL_3:2; :: thesis: verum