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