let L be complete LATTICE; :: thesis: ( InclPoset () is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] )
thus ( InclPoset () is continuous implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] ) by Lm10; :: thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] ) implies InclPoset () is continuous )
assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(),():] ; :: thesis: InclPoset () is continuous
now :: thesis: for SL being Scott TopAugmentation of L
for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SL be Scott TopAugmentation of L; :: thesis: for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]

let S be complete LATTICE; :: thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; :: thesis: sigma [:S,L:] = the topology of [:SS,SL:]
( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of (), the InternalRel of () #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;
then A2: TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13;
( RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (), the InternalRel of () #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def 4;
then TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13;
then [:SS,SL:] = [:(),():] by ;
hence sigma [:S,L:] = the topology of [:SS,SL:] by A1; :: thesis: verum
end;
hence InclPoset () is continuous by Lm11; :: thesis: verum