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
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) )
thus ex_inf_of f .: F,T by YELLOW_0:17; :: thesis: "/\" (f .: F),T = f . ("/\" F,S)
A3: 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 A4: x <= y ; :: thesis: f . x <= f . y
( uparrow (f . x) is closed & f . x <= f . x ) by Th4;
then ( f " (uparrow (f . x)) is closed & f . x in uparrow (f . x) & x in the carrier of S ) by A1, PRE_TOPC:def 12, WAYBEL_0:18;
then ( f " (uparrow (f . x)) is upper & x in f " (uparrow (f . x)) ) by Th6, FUNCT_2:46;
then ( y in f " (uparrow (f . x)) & f is Function of the carrier of S,the carrier of T ) by A4, WAYBEL_0:def 20;
then f . y in uparrow (f . x) by FUNCT_2:46;
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 set such that
A5: ( a in the carrier of S & a in F & x = f . a ) by FUNCT_2:115;
reconsider a = a as Element of S by A5;
inf F is_<=_than F by YELLOW_0:33;
then inf F <= a by A5, LATTICE3:def 8;
hence f . (inf F) <= x by A3, A5, WAYBEL_1:def 2; :: thesis: verum

end;

then A6: f . (inf F) <= inf (f .: F) by YELLOW_0:33;
reconsider BB = { ((uparrow x) ` ) where x is Element of S : verum } as prebasis of S by Def1;
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
A7: A = (uparrow x) ` ;
assume inf F in A ; :: thesis: F meets A
then not inf F >= x by A7, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of S such that
A8: ( y in F & not y >= x ) by LATTICE3:def 8;
y in A by A7, A8, YELLOW_9:1;
hence F meets A by A8, XBOOLE_0:3; :: thesis: verum

end;

then A9: inf F in Cl F by A2, Th10;
uparrow (inf (f .: F)) is closed by Th4;
then A10: f " (uparrow (inf (f .: F))) is closed by A1, PRE_TOPC:def 12;
F c= f " (uparrow (inf (f .: F)))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in f " (uparrow (inf (f .: F))) )
assume A11: 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 A11, FUNCT_2:43;
then inf (f .: F) <= f . s by YELLOW_2:24;
then f . s in uparrow (inf (f .: F)) by WAYBEL_0:18;
hence x in f " (uparrow (inf (f .: F))) by FUNCT_2:46; :: thesis: verum

end;

then Cl F c= Cl (f " (uparrow (inf (f .: F)))) by PRE_TOPC:49;
then Cl F c= f " (uparrow (inf (f .: F))) by A10, PRE_TOPC:52;
then f . (inf F) in uparrow (inf (f .: F)) by A9, FUNCT_2:46;
then f . (inf F) >= inf (f .: F) by WAYBEL_0:18;
hence inf (f .: F) = f . (inf F) by A6, ORDERS_2:25; :: thesis: verum