let S be complete LATTICE; :: thesis: ex F being Function of (UPS S,(BoolePoset 1)),(InclPoset (sigma S)) st
( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) )
set T = BoolePoset 1;
consider S' being Scott TopAugmentation of S;
reconsider T' = Omega Sierpinski_Space as Scott TopAugmentation of BoolePoset 1 by Th31, WAYBEL26:4;
( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & BoolePoset 1 = RelStr(# the carrier of T',the InternalRel of T' #) ) by YELLOW_9:def 4;
then A1: UPS S,(BoolePoset 1) = UPS S',T' by Th25
.= SCMaps S',T' by Th24
.= ContMaps S',T' by WAYBEL24:38
.= oContMaps S',Sierpinski_Space by WAYBEL26:def 1 ;
A2: the topology of S' = sigma S by YELLOW_9:51;
then consider G being Function of (InclPoset (sigma S)),(UPS S,(BoolePoset 1)) such that
A3: G is isomorphic and
A4: for V being open Subset of S' holds G . V = chi V,the carrier of S' by A1, WAYBEL26:5;
take F = G " ; :: thesis: ( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) )
A5: ( G is one-to-one & rng G = [#] (UPS S,(BoolePoset 1)) ) by A3, WAYBEL_0:66;
then A6: F = G " by TOPS_2:def 4;
hence F is isomorphic by A3, WAYBEL_0:68; :: thesis: for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1}
let f be directed-sups-preserving Function of S,(BoolePoset 1); :: thesis: F . f = f " {1}
f in the carrier of (UPS S,(BoolePoset 1)) by Def4;
then consider V being set such that
A7: ( V in dom G & f = G . V ) by A5, FUNCT_1:def 5;
dom G = the carrier of (InclPoset (sigma S)) by FUNCT_2:def 1
.= sigma S by YELLOW_1:1 ;
then reconsider V = V as open Subset of S' by A2, A7, PRE_TOPC:def 5;
thus F . f = V by A5, A6, A7, FUNCT_1:56
.= (chi V,the carrier of S') " {1} by Th13
.= f " {1} by A4, A7 ; :: thesis: verum