let S, T be complete lower TopLattice; 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; ( f is continuous implies f is filtered-infs-preserving )
assume A1:
f is continuous
; f is filtered-infs-preserving
let F be Subset of S; WAYBEL_0:def 36 ( 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
; WAYBEL_0:def 30 ( 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
then A6:
inf F in Cl F
by A2, Th10;
A7:
f is monotone
f . (inf F) is_<=_than f .: F
then A13:
f . (inf F) <= inf (f .: F)
by YELLOW_0:33;
thus
ex_inf_of f .: F,T
by YELLOW_0:17; "/\" ((f .: F),T) = f . ("/\" (F,S))
F c= f " (uparrow (inf (f .: F)))
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; verum