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

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

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

A6:
h is infs-preserving
by A3, WAYBEL_0:def 32, A4, WAYBEL_0:65;
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;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

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