let S, T be complete Lawson TopLattice; :: thesis:
A1: [#] T <> {} ;
consider Ss being Scott TopAugmentation of S, Ts being Scott TopAugmentation of T, Sl being correct lower TopAugmentation of S, Tl being correct lower TopAugmentation of T;
( S is TopAugmentation of S & T is TopAugmentation of T ) by YELLOW_9:44;
then A2: ( S is Refinement of Ss,Sl & T is Refinement of Ts,Tl ) by WAYBEL19:29;
A3: ( T is TopAugmentation of Ts & S is TopAugmentation of Ss ) by YELLOW_9:45;
A4: ( RelStr(# the carrier of Ss,the InternalRel of Ss #) = RelStr(# the carrier of S,the InternalRel of S #) & RelStr(# the carrier of Sl,the InternalRel of Sl #) = RelStr(# the carrier of S,the InternalRel of S #) & RelStr(# the carrier of Ts,the InternalRel of Ts #) = RelStr(# the carrier of T,the InternalRel of T #) & RelStr(# the carrier of Tl,the InternalRel of Tl #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:def 4;
let f be meet-preserving Function of S,T; :: thesis:
reconsider g = f as Function of Sl,Tl by A4;
reconsider h = f as Function of Ss,Ts by A4;
A5: [#] Ts <> {} ;

hereby :: thesis:

assume A6: f is continuous ; :: thesis:

let P be Subset of Ts; :: thesis:
reconsider A = P as Subset of Ts ;
reconsider C = A as Subset of T by A4;
assume A7: P is open ; :: thesis:
then C is open by A3, WAYBEL19:37;
then A8: f " C is open by A1, A6, TOPS_2:55;
( A is upper & h is monotone ) by A4, A7, WAYBEL11:def 4, WAYBEL_9:1;
then h " A is upper by WAYBEL17:2;
then f " C is upper by A4, WAYBEL_0:25;
hence h " P is open by A3, A8, WAYBEL19:41; :: thesis:

end;

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

let F be non empty filtered Subset of S; :: thesis:
assume ex_inf_of F,S ; :: according to WAYBEL_0:def 30 :: thesis:
thus ex_inf_of f .: F,T by YELLOW_0:17; :: thesis:
{(inf F)} = Lim (F opp+id ) by WAYBEL19:43;
then ( Im f,(inf F) c= Lim (f * (F opp+id )) & f is Function of the carrier of S,the carrier of T ) by A6, Th24;
then {(f . (inf F))} c= Lim (f * (F opp+id )) by SETWISEO:13;
then A9: f . (inf F) in Lim (f * (F opp+id )) by ZFMISC_1:37;
reconsider G = f .: F as non empty filtered Subset of T by WAYBEL20:25;
A10: 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:94
.= G by RELAT_1:148 ;
Lim (f * (F opp+id )) = {(inf (f * (F opp+id )))} by Th44
.= {(Inf )} by WAYBEL_9:def 2
.= {(inf G)} by A10, YELLOW_2:def 6 ;
hence "/\" (f .: F),T = f . ("/\" F,S) by A9, TARSKI:def 1; :: thesis:

end;

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

end;