let S, T be non empty complete lower TopLattice; :: thesis: for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds
f is continuous
reconsider BB = { ((uparrow x) ` ) where x is Element of T : verum } as prebasis of T by Def1;
let f be Function of S,T; :: thesis: ( ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous )
assume A1: for X being non empty Subset of S holds f preserves_inf_of X ; :: thesis: f is continuous

now

let A be Subset of T; :: thesis: ( A in BB implies f " (b₁ ` ) is closed )
A2: ex_inf_of f " (A ` ),S by YELLOW_0:17;
A3: ex_inf_of A ` ,T by YELLOW_0:17;
A4: ex_inf_of f .: (f " (A ` )),T by YELLOW_0:17;
assume A in BB ; :: thesis: f " (b₁ ` ) is closed
then consider x being Element of T such that
A5: A = (uparrow x) ` ;
set s = inf (f " (uparrow x));

per cases ( f " (A ` ) = {} S or f " (A ` ) <> {} ) ;

suppose f " (A ` ) = {} S ; :: thesis: f " (b<sub>1</sub> ` ) is closed

hence f " (A ` ) is closed by TOPS_1:22; :: thesis: verum

end;

suppose f " (A ` ) <> {} ; :: thesis: f " (b<sub>1</sub> ` ) is closed

then f preserves_inf_of f " (A ` ) by A1;
then A6: f . (inf (f " (uparrow x))) = inf (f .: (f " (A ` ))) by A5, A2, WAYBEL_0:def 30;
inf (A ` ) = x by A5, WAYBEL_0:39;
then A7: x <= f . (inf (f " (uparrow x))) by A6, A3, A4, FUNCT_1:145, YELLOW_0:35;
f " (A ` ) = uparrow (inf (f " (uparrow x)))

proof

thus f " (A ` ) c= uparrow (inf (f " (uparrow x))) :: according to XBOOLE_0:def 10 :: thesis: uparrow (inf (f " (uparrow x))) c= f " (A ` )

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in f " (A ` ) or a in uparrow (inf (f " (uparrow x))) )
assume A8: a in f " (A ` ) ; :: thesis: a in uparrow (inf (f " (uparrow x)))
then reconsider a = a as Element of S ;
inf (f " (uparrow x)) <= a by A5, A8, YELLOW_2:24;
hence a in uparrow (inf (f " (uparrow x))) by WAYBEL_0:18; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in uparrow (inf (f " (uparrow x))) or a in f " (A ` ) )
assume A9: a in uparrow (inf (f " (uparrow x))) ; :: thesis: a in f " (A ` )
then reconsider a = a as Element of S ;
f preserves_inf_of {(inf (f " (uparrow x))),a} by A1;
then A10: f . ((inf (f " (uparrow x))) "/\" a) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by YELLOW_3:8;
inf (f " (uparrow x)) <= a by A9, WAYBEL_0:18;
then f . (inf (f " (uparrow x))) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by A10, YELLOW_5:10;
then f . (inf (f " (uparrow x))) <= f . a by YELLOW_0:23;
then x <= f . a by A7, ORDERS_2:26;
then f . a in uparrow x by WAYBEL_0:18;
hence a in f " (A ` ) by A5, FUNCT_2:46; :: thesis: verum

end;

hence f " (A ` ) is closed by Th4; :: thesis: verum

end;

end;

end;

hence f is continuous by YELLOW_9:35; :: thesis: verum