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