let N be complete meet-continuous Lawson TopLattice; :: thesis: ( InclPoset (sigma N) is continuous implies N is topological_semilattice )
assume A1: InclPoset (sigma N) is continuous ; :: thesis: N is topological_semilattice
let g be Function of [:N,N:],N; :: according to YELLOW13:def 5 :: thesis: ( not R17(the carrier of [:N,N:],the carrier of N,the carrier of [:N,N:],the carrier of N,g, inf_op N) or g is continuous )
assume A2: g = inf_op N ; :: thesis: g is continuous
consider NN being correct Lawson TopAugmentation of [:N,N:];
A3: RelStr(# the carrier of NN,the InternalRel of NN #) = RelStr(# the carrier of [:N,N:],the InternalRel of [:N,N:] #) by YELLOW_9:def 4;
then reconsider h = inf_op N as Function of NN,N ;
A4: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of N,the InternalRel of N #) ;
A5: h is infs-preserving

proof

let X be Subset of NN; :: according to WAYBEL_0:def 32 :: thesis: h preserves_inf_of X
reconsider X1 = X as Subset of [:N,N:] by A3;
inf_op N preserves_inf_of X1 by WAYBEL_0:def 32;
hence h preserves_inf_of X by A3, A4, WAYBEL_0:65; :: thesis: verum

end;

then A6: h is SemilatticeHomomorphism of NN,N by WAYBEL21:5;
h is directed-sups-preserving

proof

let X be Subset of NN; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or h preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: h preserves_sup_of X
then reconsider X1 = X as non empty directed Subset of [:N,N:] by A3, WAYBEL_0:3;
inf_op N preserves_sup_of X1 by WAYBEL_0:def 37;
hence h preserves_sup_of X by A3, A4, WAYBEL_0:65; :: thesis: verum

end;

then A7: h is continuous by A5, A6, WAYBEL21:46;
A8: TopStruct(# the carrier of N,the topology of N #) = TopStruct(# the carrier of N,the topology of N #) ;
N is TopAugmentation of N by YELLOW_9:44;
then TopStruct(# the carrier of NN,the topology of NN #) = [:N,N:] by A1, Th20;
hence g is continuous by A2, A7, A8, YELLOW12:36; :: thesis: verum