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 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 ; :: 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 such that
A3: k in the carrier of (CompactSublatt T) and
A4: t <= k and
A5: k <= t' 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 by WAYBEL_3:def 2;
A7: d . t <= d . k by A4, WAYBEL_1:def 2;
d . k <= d . t' by A5, WAYBEL_1:def 2;
hence d . t << d . t' by A6, A7, WAYBEL_3:2; :: thesis: verum