let S, T be lower-bounded with_suprema Poset; :: thesis: for f being Function of S,T st f is join-preserving & f is bottom-preserving holds
f is finite-sups-preserving
let f be Function of S,T; :: thesis: ( f is join-preserving & f is bottom-preserving implies f is finite-sups-preserving )
assume A1: ( f is join-preserving & f is bottom-preserving ) ; :: thesis: f is finite-sups-preserving
let X be finite Subset of S; :: according to WAYBEL34:def 15 :: thesis: f preserves_sup_of X
A2: X is finite ;
defpred S₁[ set ] means for Y being finite Subset of S st Y = $1 holds
f preserves_sup_of Y;
f preserves_sup_of {} S by A1, Def16;
then A3: S₁[ {} ] ;
A4: for x, B being set st x in X & B c= X & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in X & B c= X & S₁[B] implies S₁[B \/ {x}] )
assume that
( x in X & B c= X ) and
A5: for Y being finite Subset of S st Y = B holds
f preserves_sup_of Y ; :: thesis: S₁[B \/ {x}]
let Y be finite Subset of S; :: thesis: ( Y = B \/ {x} implies f preserves_sup_of Y )
assume A6: Y = B \/ {x} ; :: thesis: f preserves_sup_of Y
A7: ( B c= Y & {x} c= Y ) by A6, XBOOLE_1:7;
then reconsider Z = B as finite Subset of S by XBOOLE_1:1;
A8: x in Y by A7, ZFMISC_1:37;
then reconsider x = x as Element of S ;
A9: f preserves_sup_of Z by A5;
( f .: Z = {} or ( f .: Z <> {} & f .: Z is finite ) ) ;
then A10: ( ex_sup_of f .: Z,T & ex_sup_of {(f . x)},T ) by YELLOW_0:42, YELLOW_0:54;
( Z = {} or Z <> {} ) ;
then A11: ex_sup_of Z,S by YELLOW_0:42, YELLOW_0:54;
A12: f preserves_sup_of {(sup Z),x} by A1, WAYBEL_0:def 35;
A13: ( sup {x} = x & ex_sup_of {x},S ) by YELLOW_0:38, YELLOW_0:39;
A14: ex_sup_of Y,S by A8, YELLOW_0:54;
assume ex_sup_of Y,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: Y,T & "\/" (f .: Y),T = f . ("\/" Y,S) )
f . x in f .: Y by A8, FUNCT_2:43;
hence ex_sup_of f .: Y,T by YELLOW_0:54; :: thesis: "\/" (f .: Y),T = f . ("\/" Y,S)
dom f = the carrier of S by FUNCT_2:def 1;
then Im f,x = {(f . x)} by FUNCT_1:117;
then ( f .: Y = (f .: Z) \/ {(f . x)} & sup {(f . x)} = f . x ) by A6, RELAT_1:153, YELLOW_0:39;
hence sup (f .: Y) = (sup (f .: Z)) "\/" (f . x) by A10, YELLOW_2:3
.= (f . (sup Z)) "\/" (f . x) by A9, A11, WAYBEL_0:def 31
.= f . ((sup Z) "\/" x) by A12, YELLOW_3:9
.= f . (sup Y) by A6, A11, A13, A14, YELLOW_0:36 ;
:: thesis: verum

end;

S₁[X] from FINSET_1:sch 2(A2, A3, A4);
hence f preserves_sup_of X ; :: thesis: verum