let S, T be complete lower TopLattice; :: thesis:
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:
assume A1: f is continuous ; :: thesis:
let F be Subset of S; :: according to WAYBEL_0:def 36 :: thesis:
assume that
A2: ( not F is empty & F is filtered ) and
ex_inf_of F,S ; :: according to WAYBEL_0:def 30 :: thesis:
for A being Subset of S st A in BB & inf F in A holds
F meets A

let A be Subset of S; :: thesis:
assume A in BB ; :: thesis:
then consider x being Element of S such that
A3: A = (uparrow x) ` ;
assume inf F in A ; :: thesis:
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:

end;

end;

let x be Element of T; :: according to LATTICE3:def 8 :: thesis:
assume x in f .: F ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in F ; :: thesis:
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:

end;