let N be complete Lawson meet-continuous TopLattice; :: thesis: ( InclPoset (sigma N) is continuous implies N is topological_semilattice )
assume A1: InclPoset (sigma N) is continuous ; :: thesis: 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
proof
let X be Subset of the correct Lawson TopAugmentation of [:N,N:]; :: 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;
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; :: 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 g = inf_op N ; :: thesis: g is continuous
hence g is continuous by A2, A7, A8, YELLOW12:36; :: thesis: verum