let S, T be complete lower TopLattice; :: thesis: for f being Function of S,T st f is continuous holds
f is filtered-infs-preserving
reconsider BB = { ((uparrow x) `) where x is Element of S : verum } as prebasis of S by Def1;
let f be Function of S,T; :: thesis: ( f is continuous implies f is filtered-infs-preserving )
assume A1: f is continuous ; :: thesis: f is filtered-infs-preserving
let F be Subset of S; :: according to WAYBEL_0:def 36 :: thesis: ( F is empty or not F is filtered or f preserves_inf_of F )
assume that
A2: ( not F is empty & F is filtered ) and
ex_inf_of F,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: F,T & "/\" ((f .: F),T) = f . ("/\" (F,S)) )
for A being Subset of S st A in BB & inf F in A holds
F meets A

proof

let A be Subset of S; :: thesis: ( A in BB & inf F in A implies F meets A )
assume A in BB ; :: thesis: ( not inf F in A or F meets A )
then consider x being Element of S such that
A3: A = (uparrow x) ` ;
assume inf F in A ; :: thesis: F meets A
then not inf F >= x by A3, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of S such that
A4: y in F and
A5: not y >= x ;
y in A by A3, A5, YELLOW_9:1;
hence F meets A by A4, XBOOLE_0:3; :: thesis: verum

end;

then A6: inf F in Cl F by A2, Th10;
A7: f is monotone

proof

let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f . x <= f . y )
assume A8: x <= y ; :: thesis: f . x <= f . y
f . x <= f . x ;
then f . x in uparrow (f . x) by WAYBEL_0:18;
then A9: x in f " (uparrow (f . x)) by FUNCT_2:38;
uparrow (f . x) is closed by Th4;
then f " (uparrow (f . x)) is closed by A1;
then f " (uparrow (f . x)) is upper by Th6;
then y in f " (uparrow (f . x)) by A9, A8;
then f . y in uparrow (f . x) by FUNCT_2:38;
hence f . x <= f . y by WAYBEL_0:18; :: thesis: verum

end;

f . (inf F) is_<=_than f .: F

proof

let x be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not x in f .: F or f . (inf F) <= x )
assume x in f .: F ; :: thesis: f . (inf F) <= x
then consider a being object such that
A10: a in the carrier of S and
A11: a in F and
A12: x = f . a by FUNCT_2:64;
reconsider a = a as Element of S by A10;
inf F is_<=_than F by YELLOW_0:33;
then inf F <= a by A11;
hence f . (inf F) <= x by A7, A12; :: thesis: verum

end;

then A13: f . (inf F) <= inf (f .: F) by YELLOW_0:33;
thus ex_inf_of f .: F,T by YELLOW_0:17; :: thesis: "/\" ((f .: F),T) = f . ("/\" (F,S))
F c= f " (uparrow (inf (f .: F)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in f " (uparrow (inf (f .: F))) )
assume A14: x in F ; :: thesis: x in f " (uparrow (inf (f .: F)))
then reconsider s = x as Element of S ;
f . s in f .: F by A14, FUNCT_2:35;
then inf (f .: F) <= f . s by YELLOW_2:22;
then f . s in uparrow (inf (f .: F)) by WAYBEL_0:18;
hence x in f " (uparrow (inf (f .: F))) by FUNCT_2:38; :: thesis: verum

end;

then A15: Cl F c= Cl (f " (uparrow (inf (f .: F)))) by PRE_TOPC:19;
uparrow (inf (f .: F)) is closed by Th4;
then f " (uparrow (inf (f .: F))) is closed by A1;
then Cl F c= f " (uparrow (inf (f .: F))) by A15, PRE_TOPC:22;
then f . (inf F) in uparrow (inf (f .: F)) by A6, FUNCT_2:38;
then f . (inf F) >= inf (f .: F) by WAYBEL_0:18;
hence inf (f .: F) = f . (inf F) by A13, ORDERS_2:2; :: thesis: verum