let N be complete Lawson meet-continuous TopLattice; :: thesis: ( InclPoset () is continuous implies N is topological_semilattice )
assume A1: InclPoset () is continuous ; :: thesis:
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 ;
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:
then reconsider X1 = X as non empty directed Subset of [:N,N:] by ;
inf_op N preserves_sup_of X1 by WAYBEL_0:def 37;
hence h preserves_sup_of X by ; :: thesis: verum
end;
A6: h is infs-preserving by ;
then h is SemilatticeHomomorphism of the correct Lawson TopAugmentation of [:N,N:],N by WAYBEL21:5;
then A7: h is continuous by ;
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 ; :: thesis: verum