let N be complete Lawson meet-continuous TopLattice; ( InclPoset (sigma N) is continuous implies N is topological_semilattice )
assume A1:
InclPoset (sigma N) is continuous
; N is topological_semilattice
set NN = the correct Lawson TopAugmentation of [:N,N:];
N is TopAugmentation of N
by YELLOW_9:44;
then A2:
TopStruct(# the carrier of the correct Lawson TopAugmentation of [:N,N:], the topology of the correct Lawson TopAugmentation of [:N,N:] #) = [:N,N:]
by A1, Th20;
A3:
RelStr(# the carrier of the correct Lawson TopAugmentation of [:N,N:], the InternalRel of the correct Lawson TopAugmentation of [:N,N:] #) = 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 the correct Lawson TopAugmentation of [:N,N:],N ;
A4:
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N, the InternalRel of N #)
;
A5:
h is directed-sups-preserving
A6:
h is infs-preserving
by A3, WAYBEL_0:def 32, A4, WAYBEL_0:65;
then
h is SemilatticeHomomorphism of the correct Lawson TopAugmentation of [:N,N:],N
by WAYBEL21:5;
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 #)
;
let g be Function of [:N,N:],N; YELLOW13:def 5 ( 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
g = inf_op N
; g is continuous
hence
g is continuous
by A2, A7, A8, YELLOW12:36; verum