set T = BoolePoset 1;
reconsider T9 = Omega Sierpinski_Space as Scott TopAugmentation of BoolePoset 1 by Th31, WAYBEL26:4;
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} ) )
consider S9 being Scott TopAugmentation of S;
A1: BoolePoset 1 = RelStr(# the carrier of T9, the InternalRel of T9 #) by YELLOW_9:def 4;
A2: the topology of S9 = sigma S by YELLOW_9:51;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) by YELLOW_9:def 4;
then UPS (S,(BoolePoset 1)) = UPS (S9,T9) by A1, Th25
.= SCMaps (S9,T9) by Th24
.= ContMaps (S9,T9) by WAYBEL24:38
.= oContMaps (S9,Sierpinski_Space) by WAYBEL26:def 1 ;
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 S9 holds G . V = chi (V, the carrier of S9) by A2, 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: rng G = [#] (UPS (S,(BoolePoset 1))) by A3, WAYBEL_0:66;
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 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 and
A8: 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 S9 by A2, A7, PRE_TOPC:def 5;
thus F . f = V by A3, A6, A7, A8, FUNCT_1:56
.= (chi (V, the carrier of S9)) " {1} by Th13
.= f " {1} by A4, A8 ; :: thesis: verum