let S, T be complete Lawson TopLattice; :: thesis: for f being meet-preserving Function of S,T holds
( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
A1: [#] T <> {} ;
set Ss = the Scott TopAugmentation of S;
set Ts = the Scott TopAugmentation of T;
set Sl = the correct lower TopAugmentation of S;
set Tl = the correct lower TopAugmentation of T;
A2: S is TopAugmentation of S by YELLOW_9:44;
A3: T is TopAugmentation of T by YELLOW_9:44;
A4: S is Refinement of the Scott TopAugmentation of S, the correct lower TopAugmentation of S by A2, WAYBEL19:29;
A5: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by A3, WAYBEL19:29;
A6: T is TopAugmentation of the Scott TopAugmentation of T by YELLOW_9:45;
A7: S is TopAugmentation of the Scott TopAugmentation of S by YELLOW_9:45;
A8: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
A9: RelStr(# the carrier of the correct lower TopAugmentation of S, the InternalRel of the correct lower TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
A11: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
let f be meet-preserving Function of S,T; :: thesis: ( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
reconsider g = f as Function of the correct lower TopAugmentation of S, the correct lower TopAugmentation of T by A9, A11;
reconsider h = f as Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A8, A10;
A12: [#] the Scott TopAugmentation of T <> {} ;

hereby :: thesis: ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous )

assume A13: f is continuous ; :: thesis: ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) )

now :: thesis: for P being Subset of the Scott TopAugmentation of T st P is open holds
h " P is open

let P be Subset of the Scott TopAugmentation of T; :: thesis: ( P is open implies h " P is open )
reconsider A = P as Subset of the Scott TopAugmentation of T ;
reconsider C = A as Subset of T by A10;
assume A14: P is open ; :: thesis: h " P is open
then C is open by A6, WAYBEL19:37;
then A15: f " C is open by A1, A13, TOPS_2:43;
A is upper by A14, WAYBEL11:def 4;
then h " A is upper by A8, A10, WAYBEL17:2, WAYBEL_9:1;
then f " C is upper by A8, WAYBEL_0:25;
hence h " P is open by A7, A15, WAYBEL19:41; :: thesis: verum

end;

then h is continuous by A12, TOPS_2:43;
hence f is directed-sups-preserving by A8, A10, Th6; :: thesis: for X being non empty Subset of S holds f preserves_inf_of X
for X being non empty filtered Subset of S holds f preserves_inf_of X

proof

let F be non empty filtered Subset of S; :: thesis: f preserves_inf_of F
assume 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))
{(inf F)} = Lim (F opp+id) by WAYBEL19:43;
then Im (f,(inf F)) c= Lim (f * (F opp+id)) by A13, Th24;
then {(f . (inf F))} c= Lim (f * (F opp+id)) by SETWISEO:8;
then A16: f . (inf F) in Lim (f * (F opp+id)) by ZFMISC_1:31;
reconsider G = f .: F as non empty filtered Subset of T by WAYBEL20:24;
A17: rng the mapping of (f * (F opp+id)) = rng (f * the mapping of (F opp+id)) by WAYBEL_9:def 8
.= rng (f * (id F)) by WAYBEL19:27
.= rng (f | F) by RELAT_1:65
.= G by RELAT_1:115 ;
Lim (f * (F opp+id)) = {(inf (f * (F opp+id)))} by Th44
.= {(Inf )} by WAYBEL_9:def 2
.= {(inf G)} by A17, YELLOW_2:def 6 ;
hence "/\" ((f .: F),T) = f . ("/\" (F,S)) by A16, TARSKI:def 1; :: thesis: verum

end;

hence for X being non empty Subset of S holds f preserves_inf_of X by Th4; :: thesis: verum

end;

assume f is directed-sups-preserving ; :: thesis: ( ex X being non empty Subset of S st not f preserves_inf_of X or f is continuous )
then A18: h is directed-sups-preserving by A8, A10, Th6;
assume for X being non empty Subset of S holds f preserves_inf_of X ; :: thesis: f is continuous
then for X being non empty Subset of the correct lower TopAugmentation of S holds g preserves_inf_of X by A9, A11, WAYBEL_0:65;
then g is continuous by WAYBEL19:8;
hence f is continuous by A4, A5, A18, WAYBEL19:24; :: thesis: verum