let L be complete LATTICE; :: thesis: ( S_{7}[L] implies S_{8}[L] )

assume A1: S_{7}[L]
; :: thesis: S_{8}[L]

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:]

A2: RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;

UPS (L,(BoolePoset {0})) is non empty full SubRelStr of (BoolePoset {0}) |^ the carrier of L by WAYBEL27:def 4;

then A3: (UPS (L,(BoolePoset {0}))) |^ the carrier of S is non empty full SubRelStr of ((BoolePoset {0}) |^ the carrier of L) |^ the carrier of S by YELLOW16:39;

UPS (S,(UPS (L,(BoolePoset {0})))) is non empty full SubRelStr of (UPS (L,(BoolePoset {0}))) |^ the carrier of S by WAYBEL27:def 4;

then A4: UPS (S,(UPS (L,(BoolePoset {0})))) is non empty full SubRelStr of ((BoolePoset {0}) |^ the carrier of L) |^ the carrier of S by A3, WAYBEL15:1;

consider f5 being Function of (UPS (L,(BoolePoset {0}))),(InclPoset (sigma L)) such that

A5: f5 is isomorphic and

A6: for f being directed-sups-preserving Function of L,(BoolePoset {0}) holds f5 . f = f " {1} by WAYBEL27:33;

set f6 = UPS ((id S),f5);

consider f3 being Function of (UPS (S,(UPS (L,(BoolePoset {0}))))),(UPS ([:S,L:],(BoolePoset {0}))) such that

A7: ( f3 is uncurrying & f3 is isomorphic ) by WAYBEL27:47;

set f4 = f3 " ;

set T = Sigma (InclPoset the topology of SL);

consider f1 being Function of (UPS ([:S,L:],(BoolePoset {0}))),(InclPoset (sigma [:S,L:])) such that

A8: f1 is isomorphic and

A9: for f being directed-sups-preserving Function of [:S,L:],(BoolePoset {0}) holds f1 . f = f " {1} by WAYBEL27:33;

A10: f3 " is isomorphic by A7, YELLOW14:10;

set f2 = f1 " ;

set G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ");

A11: the topology of SL = sigma L by YELLOW_9:51;

then A12: RelStr(# the carrier of (Sigma (InclPoset the topology of SL)), the InternalRel of (Sigma (InclPoset the topology of SL)) #) = RelStr(# the carrier of (InclPoset (sigma L)), the InternalRel of (InclPoset (sigma L)) #) by YELLOW_9:def 4;

A13: the carrier of (UPS (S,(InclPoset (sigma L)))) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))

set F = Theta (SS,SL);

A17: RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4;

( (BoolePoset {0}) |^ the carrier of [:S,L:] = (BoolePoset {0}) |^ [: the carrier of S, the carrier of L:] & UPS ([:S,L:],(BoolePoset {0})) is non empty full SubRelStr of (BoolePoset {0}) |^ the carrier of [:S,L:] ) by WAYBEL27:def 4, YELLOW_3:def 2;

then A18: f3 " is currying by A7, A4, Th2;

A19: for V being Element of (InclPoset (sigma [:S,L:]))

for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V }_{6}[SL]
by A1, A11, Lm8;

then S_{4}[SL]
by Lm6;

then A33: Theta (SS,SL) is isomorphic by Lm3;

A34: the carrier of (InclPoset (sigma [:S,L:])) c= the carrier of (InclPoset the topology of [:SS,SL:])

then UPS ((id S),f5) is isomorphic by A5, WAYBEL27:35;

then A46: (UPS ((id S),f5)) * (f3 ") is isomorphic by A10, Th6;

A47: f1 " is isomorphic by A8, YELLOW14:10;

the carrier of (InclPoset the topology of [:SS,SL:]) c= the carrier of (InclPoset (sigma [:S,L:]))

hence sigma [:S,L:] = the carrier of (InclPoset the topology of [:SS,SL:]) by YELLOW_1:1

.= the topology of [:SS,SL:] by YELLOW_1:1 ;

:: thesis: verum

assume A1: S

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:]

A2: RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;

UPS (L,(BoolePoset {0})) is non empty full SubRelStr of (BoolePoset {0}) |^ the carrier of L by WAYBEL27:def 4;

then A3: (UPS (L,(BoolePoset {0}))) |^ the carrier of S is non empty full SubRelStr of ((BoolePoset {0}) |^ the carrier of L) |^ the carrier of S by YELLOW16:39;

UPS (S,(UPS (L,(BoolePoset {0})))) is non empty full SubRelStr of (UPS (L,(BoolePoset {0}))) |^ the carrier of S by WAYBEL27:def 4;

then A4: UPS (S,(UPS (L,(BoolePoset {0})))) is non empty full SubRelStr of ((BoolePoset {0}) |^ the carrier of L) |^ the carrier of S by A3, WAYBEL15:1;

consider f5 being Function of (UPS (L,(BoolePoset {0}))),(InclPoset (sigma L)) such that

A5: f5 is isomorphic and

A6: for f being directed-sups-preserving Function of L,(BoolePoset {0}) holds f5 . f = f " {1} by WAYBEL27:33;

set f6 = UPS ((id S),f5);

consider f3 being Function of (UPS (S,(UPS (L,(BoolePoset {0}))))),(UPS ([:S,L:],(BoolePoset {0}))) such that

A7: ( f3 is uncurrying & f3 is isomorphic ) by WAYBEL27:47;

set f4 = f3 " ;

set T = Sigma (InclPoset the topology of SL);

consider f1 being Function of (UPS ([:S,L:],(BoolePoset {0}))),(InclPoset (sigma [:S,L:])) such that

A8: f1 is isomorphic and

A9: for f being directed-sups-preserving Function of [:S,L:],(BoolePoset {0}) holds f1 . f = f " {1} by WAYBEL27:33;

A10: f3 " is isomorphic by A7, YELLOW14:10;

set f2 = f1 " ;

set G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ");

A11: the topology of SL = sigma L by YELLOW_9:51;

then A12: RelStr(# the carrier of (Sigma (InclPoset the topology of SL)), the InternalRel of (Sigma (InclPoset the topology of SL)) #) = RelStr(# the carrier of (InclPoset (sigma L)), the InternalRel of (InclPoset (sigma L)) #) by YELLOW_9:def 4;

A13: the carrier of (UPS (S,(InclPoset (sigma L)))) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))

proof

then reconsider G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ") as Function of (InclPoset (sigma [:S,L:])),(ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ;
thus
the carrier of (UPS (S,(InclPoset (sigma L)))) c= the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) c= the carrier of (UPS (S,(InclPoset (sigma L))))

assume x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ; :: thesis: x in the carrier of (UPS (S,(InclPoset (sigma L))))

then consider x1 being Function of SS,(Sigma (InclPoset the topology of SL)) such that

A15: x1 = x and

A16: x1 is continuous by WAYBEL24:def 3;

reconsider x2 = x1 as Function of S,(InclPoset (sigma L)) by A2, A12;

x1 is directed-sups-preserving by A16, WAYBEL17:22;

then x2 is directed-sups-preserving by A2, A12, WAYBEL21:6;

hence x in the carrier of (UPS (S,(InclPoset (sigma L)))) by A15, WAYBEL27:def 4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) or x in the carrier of (UPS (S,(InclPoset (sigma L)))) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UPS (S,(InclPoset (sigma L)))) or x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) )

assume A14: x in the carrier of (UPS (S,(InclPoset (sigma L)))) ; :: thesis: x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))

then reconsider x1 = x as Function of SS,(Sigma (InclPoset the topology of SL)) by A2, A12, WAYBEL27:def 4;

x is directed-sups-preserving Function of S,(InclPoset (sigma L)) by A14, WAYBEL27:def 4;

then x1 is directed-sups-preserving by A2, A12, WAYBEL21:6;

then x1 is continuous by WAYBEL17:22;

hence x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by WAYBEL24:def 3; :: thesis: verum

end;assume A14: x in the carrier of (UPS (S,(InclPoset (sigma L)))) ; :: thesis: x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))

then reconsider x1 = x as Function of SS,(Sigma (InclPoset the topology of SL)) by A2, A12, WAYBEL27:def 4;

x is directed-sups-preserving Function of S,(InclPoset (sigma L)) by A14, WAYBEL27:def 4;

then x1 is directed-sups-preserving by A2, A12, WAYBEL21:6;

then x1 is continuous by WAYBEL17:22;

hence x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by WAYBEL24:def 3; :: thesis: verum

assume x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ; :: thesis: x in the carrier of (UPS (S,(InclPoset (sigma L))))

then consider x1 being Function of SS,(Sigma (InclPoset the topology of SL)) such that

A15: x1 = x and

A16: x1 is continuous by WAYBEL24:def 3;

reconsider x2 = x1 as Function of S,(InclPoset (sigma L)) by A2, A12;

x1 is directed-sups-preserving by A16, WAYBEL17:22;

then x2 is directed-sups-preserving by A2, A12, WAYBEL21:6;

hence x in the carrier of (UPS (S,(InclPoset (sigma L)))) by A15, WAYBEL27:def 4; :: thesis: verum

set F = Theta (SS,SL);

A17: RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4;

( (BoolePoset {0}) |^ the carrier of [:S,L:] = (BoolePoset {0}) |^ [: the carrier of S, the carrier of L:] & UPS ([:S,L:],(BoolePoset {0})) is non empty full SubRelStr of (BoolePoset {0}) |^ the carrier of [:S,L:] ) by WAYBEL27:def 4, YELLOW_3:def 2;

then A18: f3 " is currying by A7, A4, Th2;

A19: for V being Element of (InclPoset (sigma [:S,L:]))

for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V }

proof

S
let V be Element of (InclPoset (sigma [:S,L:])); :: thesis: for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V }

let s be Element of S; :: thesis: (G . V) . s = { y where y is Element of L : [s,y] in V }

reconsider fff = (f3 ") . ((f1 ") . V) as directed-sups-preserving Function of S,(UPS (L,(BoolePoset {0}))) by WAYBEL27:def 4;

reconsider f2V = (f1 ") . V as directed-sups-preserving Function of [:S,L:],(BoolePoset {0}) by WAYBEL27:def 4;

A20: ( f5 is sups-preserving & (f5 * fff) * (id the carrier of S) = f5 * fff ) by A5, FUNCT_2:17, WAYBEL13:20;

A21: ((f3 ") . ((f1 ") . V)) . s is directed-sups-preserving Function of L,(BoolePoset {0}) by WAYBEL27:def 4;

then A22: dom (((f3 ") . ((f1 ") . V)) . s) = the carrier of L by FUNCT_2:def 1;

G . V = ((UPS ((id S),f5)) * (f3 ")) . ((f1 ") . V) by FUNCT_2:15

.= (UPS ((id S),f5)) . ((f3 ") . ((f1 ") . V)) by FUNCT_2:15

.= f5 * fff by A20, WAYBEL27:def 5 ;

then A23: (G . V) . s = f5 . (fff . s) by FUNCT_2:15

.= (((f3 ") . ((f1 ") . V)) . s) " {1} by A6, A21 ;

A24: rng f1 = [#] (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def 3;

dom (f3 ") = the carrier of (UPS ([:S,L:],(BoolePoset {0}))) by FUNCT_2:def 1;

then A25: (f3 ") . ((f1 ") . V) = curry ((f1 ") . V) by A18;

rng f1 = the carrier of (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def 3;

then A26: V = (id (rng f1)) . V

.= (f1 * (f1 ")) . V by A8, A24, TOPS_2:52

.= f1 . ((f1 ") . V) by FUNCT_2:15

.= f2V " {1} by A9 ;

thus (G . V) . s c= { y where y is Element of L : [s,y] in V } :: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of L : [s,y] in V } c= (G . V) . s

assume x in { y where y is Element of L : [s,y] in V } ; :: thesis: x in (G . V) . s

then consider y being Element of L such that

A30: y = x and

A31: [s,y] in V ;

dom f2V = the carrier of [:S,L:] by FUNCT_2:def 1;

then A32: [s,y] in dom ((f1 ") . V) ;

reconsider cs = (curry ((f1 ") . V)) . s as Function ;

((f1 ") . V) . (s,y) in {1} by A26, A31, FUNCT_1:def 7;

then ((f1 ") . V) . (s,y) = 1 by TARSKI:def 1;

then cs . y = 1 by A32, FUNCT_5:20;

then (((f3 ") . ((f1 ") . V)) . s) . y in {1} by A25, TARSKI:def 1;

hence x in (G . V) . s by A23, A30, A22, FUNCT_1:def 7; :: thesis: verum

end;let s be Element of S; :: thesis: (G . V) . s = { y where y is Element of L : [s,y] in V }

reconsider fff = (f3 ") . ((f1 ") . V) as directed-sups-preserving Function of S,(UPS (L,(BoolePoset {0}))) by WAYBEL27:def 4;

reconsider f2V = (f1 ") . V as directed-sups-preserving Function of [:S,L:],(BoolePoset {0}) by WAYBEL27:def 4;

A20: ( f5 is sups-preserving & (f5 * fff) * (id the carrier of S) = f5 * fff ) by A5, FUNCT_2:17, WAYBEL13:20;

A21: ((f3 ") . ((f1 ") . V)) . s is directed-sups-preserving Function of L,(BoolePoset {0}) by WAYBEL27:def 4;

then A22: dom (((f3 ") . ((f1 ") . V)) . s) = the carrier of L by FUNCT_2:def 1;

G . V = ((UPS ((id S),f5)) * (f3 ")) . ((f1 ") . V) by FUNCT_2:15

.= (UPS ((id S),f5)) . ((f3 ") . ((f1 ") . V)) by FUNCT_2:15

.= f5 * fff by A20, WAYBEL27:def 5 ;

then A23: (G . V) . s = f5 . (fff . s) by FUNCT_2:15

.= (((f3 ") . ((f1 ") . V)) . s) " {1} by A6, A21 ;

A24: rng f1 = [#] (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def 3;

dom (f3 ") = the carrier of (UPS ([:S,L:],(BoolePoset {0}))) by FUNCT_2:def 1;

then A25: (f3 ") . ((f1 ") . V) = curry ((f1 ") . V) by A18;

rng f1 = the carrier of (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def 3;

then A26: V = (id (rng f1)) . V

.= (f1 * (f1 ")) . V by A8, A24, TOPS_2:52

.= f1 . ((f1 ") . V) by FUNCT_2:15

.= f2V " {1} by A9 ;

thus (G . V) . s c= { y where y is Element of L : [s,y] in V } :: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of L : [s,y] in V } c= (G . V) . s

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of L : [s,y] in V } or x in (G . V) . s )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (G . V) . s or x in { y where y is Element of L : [s,y] in V } )

assume A27: x in (G . V) . s ; :: thesis: x in { y where y is Element of L : [s,y] in V }

then x in dom (((f3 ") . ((f1 ") . V)) . s) by A23, FUNCT_1:def 7;

then reconsider y = x as Element of L by A21, FUNCT_2:def 1;

(((f3 ") . ((f1 ") . V)) . s) . x in {1} by A23, A27, FUNCT_1:def 7;

then A28: (((f3 ") . ((f1 ") . V)) . s) . y = 1 by TARSKI:def 1;

A29: dom f2V = the carrier of [:S,L:] by FUNCT_2:def 1;

then [s,y] in dom ((f1 ") . V) ;

then ((f1 ") . V) . (s,y) = 1 by A25, A28, FUNCT_5:20;

then ((f1 ") . V) . (s,y) in {1} by TARSKI:def 1;

then [s,y] in ((f1 ") . V) " {1} by A29, FUNCT_1:def 7;

hence x in { y where y is Element of L : [s,y] in V } by A26; :: thesis: verum

end;assume A27: x in (G . V) . s ; :: thesis: x in { y where y is Element of L : [s,y] in V }

then x in dom (((f3 ") . ((f1 ") . V)) . s) by A23, FUNCT_1:def 7;

then reconsider y = x as Element of L by A21, FUNCT_2:def 1;

(((f3 ") . ((f1 ") . V)) . s) . x in {1} by A23, A27, FUNCT_1:def 7;

then A28: (((f3 ") . ((f1 ") . V)) . s) . y = 1 by TARSKI:def 1;

A29: dom f2V = the carrier of [:S,L:] by FUNCT_2:def 1;

then [s,y] in dom ((f1 ") . V) ;

then ((f1 ") . V) . (s,y) = 1 by A25, A28, FUNCT_5:20;

then ((f1 ") . V) . (s,y) in {1} by TARSKI:def 1;

then [s,y] in ((f1 ") . V) " {1} by A29, FUNCT_1:def 7;

hence x in { y where y is Element of L : [s,y] in V } by A26; :: thesis: verum

assume x in { y where y is Element of L : [s,y] in V } ; :: thesis: x in (G . V) . s

then consider y being Element of L such that

A30: y = x and

A31: [s,y] in V ;

dom f2V = the carrier of [:S,L:] by FUNCT_2:def 1;

then A32: [s,y] in dom ((f1 ") . V) ;

reconsider cs = (curry ((f1 ") . V)) . s as Function ;

((f1 ") . V) . (s,y) in {1} by A26, A31, FUNCT_1:def 7;

then ((f1 ") . V) . (s,y) = 1 by TARSKI:def 1;

then cs . y = 1 by A32, FUNCT_5:20;

then (((f3 ") . ((f1 ") . V)) . s) . y in {1} by A25, TARSKI:def 1;

hence x in (G . V) . s by A23, A30, A22, FUNCT_1:def 7; :: thesis: verum

then S

then A33: Theta (SS,SL) is isomorphic by Lm3;

A34: the carrier of (InclPoset (sigma [:S,L:])) c= the carrier of (InclPoset the topology of [:SS,SL:])

proof

InclPoset (sigma L) = InclPoset the topology of SL
by YELLOW_9:51;
let V be object ; :: according to TARSKI:def 3 :: thesis: ( not V in the carrier of (InclPoset (sigma [:S,L:])) or V in the carrier of (InclPoset the topology of [:SS,SL:]) )

assume V in the carrier of (InclPoset (sigma [:S,L:])) ; :: thesis: V in the carrier of (InclPoset the topology of [:SS,SL:])

then reconsider V1 = V as Element of (InclPoset (sigma [:S,L:])) ;

rng (Theta (SS,SL)) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by A33, FUNCT_2:def 3;

then consider W being object such that

A35: W in dom (Theta (SS,SL)) and

A36: (Theta (SS,SL)) . W = G . V1 by FUNCT_1:def 3;

reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) by A35;

dom (Theta (SS,SL)) = the carrier of (InclPoset the topology of [:SS,SL:]) by FUNCT_2:def 1;

then W in the topology of [:SS,SL:] by A35, YELLOW_1:1;

then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;

A37: V1 c= W1

hence V in the carrier of (InclPoset the topology of [:SS,SL:]) ; :: thesis: verum

end;assume V in the carrier of (InclPoset (sigma [:S,L:])) ; :: thesis: V in the carrier of (InclPoset the topology of [:SS,SL:])

then reconsider V1 = V as Element of (InclPoset (sigma [:S,L:])) ;

rng (Theta (SS,SL)) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by A33, FUNCT_2:def 3;

then consider W being object such that

A35: W in dom (Theta (SS,SL)) and

A36: (Theta (SS,SL)) . W = G . V1 by FUNCT_1:def 3;

reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) by A35;

dom (Theta (SS,SL)) = the carrier of (InclPoset the topology of [:SS,SL:]) by FUNCT_2:def 1;

then W in the topology of [:SS,SL:] by A35, YELLOW_1:1;

then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;

A37: V1 c= W1

proof

W2 c= V1
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in V1 or v in W1 )

assume A38: v in V1 ; :: thesis: v in W1

V1 in the carrier of (InclPoset (sigma [:S,L:])) ;

then V in sigma [:S,L:] by YELLOW_1:1;

then V1 c= the carrier of [:S,L:] ;

then V1 c= [: the carrier of S, the carrier of L:] by YELLOW_3:def 2;

then consider v1, v2 being object such that

A39: v1 in the carrier of S and

A40: v2 in the carrier of L and

A41: v = [v1,v2] by A38, ZFMISC_1:84;

reconsider v2 = v2 as Element of L by A40;

reconsider v1 = v1 as Element of S by A39;

v2 in { y where y is Element of L : [v1,y] in V1 } by A38, A41;

then v2 in (G . V1) . v1 by A19;

then v2 in ((W1, the carrier of S) *graph) . v1 by A2, A36, Def3;

then v2 in Im (W1,v1) by WAYBEL26:def 5;

then ex v19 being object st

( [v19,v2] in W1 & v19 in {v1} ) by RELAT_1:def 13;

hence v in W1 by A41, TARSKI:def 1; :: thesis: verum

end;assume A38: v in V1 ; :: thesis: v in W1

V1 in the carrier of (InclPoset (sigma [:S,L:])) ;

then V in sigma [:S,L:] by YELLOW_1:1;

then V1 c= the carrier of [:S,L:] ;

then V1 c= [: the carrier of S, the carrier of L:] by YELLOW_3:def 2;

then consider v1, v2 being object such that

A39: v1 in the carrier of S and

A40: v2 in the carrier of L and

A41: v = [v1,v2] by A38, ZFMISC_1:84;

reconsider v2 = v2 as Element of L by A40;

reconsider v1 = v1 as Element of S by A39;

v2 in { y where y is Element of L : [v1,y] in V1 } by A38, A41;

then v2 in (G . V1) . v1 by A19;

then v2 in ((W1, the carrier of S) *graph) . v1 by A2, A36, Def3;

then v2 in Im (W1,v1) by WAYBEL26:def 5;

then ex v19 being object st

( [v19,v2] in W1 & v19 in {v1} ) by RELAT_1:def 13;

hence v in W1 by A41, TARSKI:def 1; :: thesis: verum

proof

then
W2 = V
by A37, XBOOLE_0:def 10;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in W2 or w in V1 )

assume A42: w in W2 ; :: thesis: w in V1

W1 c= the carrier of [:SS,SL:] ;

then W1 c= [: the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;

then consider w1, w2 being object such that

A43: w1 in the carrier of S and

A44: w2 in the carrier of L and

A45: w = [w1,w2] by A2, A17, A42, ZFMISC_1:84;

reconsider w2 = w2 as Element of L by A44;

reconsider w1 = w1 as Element of S by A43;

w1 in {w1} by TARSKI:def 1;

then w2 in Im (W1,w1) by A42, A45, RELAT_1:def 13;

then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def 5;

then w2 in ((Theta (SS,SL)) . W2) . w1 by A2, Def3;

then w2 in { y where y is Element of L : [w1,y] in V1 } by A19, A36;

then ex w29 being Element of L st

( w29 = w2 & [w1,w29] in V1 ) ;

hence w in V1 by A45; :: thesis: verum

end;assume A42: w in W2 ; :: thesis: w in V1

W1 c= the carrier of [:SS,SL:] ;

then W1 c= [: the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;

then consider w1, w2 being object such that

A43: w1 in the carrier of S and

A44: w2 in the carrier of L and

A45: w = [w1,w2] by A2, A17, A42, ZFMISC_1:84;

reconsider w2 = w2 as Element of L by A44;

reconsider w1 = w1 as Element of S by A43;

w1 in {w1} by TARSKI:def 1;

then w2 in Im (W1,w1) by A42, A45, RELAT_1:def 13;

then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def 5;

then w2 in ((Theta (SS,SL)) . W2) . w1 by A2, Def3;

then w2 in { y where y is Element of L : [w1,y] in V1 } by A19, A36;

then ex w29 being Element of L st

( w29 = w2 & [w1,w29] in V1 ) ;

hence w in V1 by A45; :: thesis: verum

hence V in the carrier of (InclPoset the topology of [:SS,SL:]) ; :: thesis: verum

then UPS ((id S),f5) is isomorphic by A5, WAYBEL27:35;

then A46: (UPS ((id S),f5)) * (f3 ") is isomorphic by A10, Th6;

A47: f1 " is isomorphic by A8, YELLOW14:10;

the carrier of (InclPoset the topology of [:SS,SL:]) c= the carrier of (InclPoset (sigma [:S,L:]))

proof

then
the carrier of (InclPoset (sigma [:S,L:])) = the carrier of (InclPoset the topology of [:SS,SL:])
by A34;
let W be object ; :: according to TARSKI:def 3 :: thesis: ( not W in the carrier of (InclPoset the topology of [:SS,SL:]) or W in the carrier of (InclPoset (sigma [:S,L:])) )

assume A48: W in the carrier of (InclPoset the topology of [:SS,SL:]) ; :: thesis: W in the carrier of (InclPoset (sigma [:S,L:]))

then reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) ;

W in the topology of [:SS,SL:] by A48, YELLOW_1:1;

then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;

G is onto by A47, A46, A13, Th6, YELLOW14:9;

then rng G = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by FUNCT_2:def 3;

then consider V being object such that

A49: V in dom G and

A50: G . V = (Theta (SS,SL)) . W2 by FUNCT_1:def 3;

reconsider V = V as Element of (InclPoset (sigma [:S,L:])) by A49;

A51: V c= W2

hence W in the carrier of (InclPoset (sigma [:S,L:])) ; :: thesis: verum

end;assume A48: W in the carrier of (InclPoset the topology of [:SS,SL:]) ; :: thesis: W in the carrier of (InclPoset (sigma [:S,L:]))

then reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) ;

W in the topology of [:SS,SL:] by A48, YELLOW_1:1;

then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;

G is onto by A47, A46, A13, Th6, YELLOW14:9;

then rng G = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by FUNCT_2:def 3;

then consider V being object such that

A49: V in dom G and

A50: G . V = (Theta (SS,SL)) . W2 by FUNCT_1:def 3;

reconsider V = V as Element of (InclPoset (sigma [:S,L:])) by A49;

A51: V c= W2

proof

W2 c= V
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in V or v in W2 )

assume A52: v in V ; :: thesis: v in W2

V in the carrier of (InclPoset (sigma [:S,L:])) ;

then V in sigma [:S,L:] by YELLOW_1:1;

then V c= the carrier of [:S,L:] ;

then V c= [: the carrier of S, the carrier of L:] by YELLOW_3:def 2;

then consider v1, v2 being object such that

A53: v1 in the carrier of S and

A54: v2 in the carrier of L and

A55: v = [v1,v2] by A52, ZFMISC_1:84;

reconsider v2 = v2 as Element of L by A54;

reconsider v1 = v1 as Element of S by A53;

v2 in { y where y is Element of L : [v1,y] in V } by A52, A55;

then v2 in (G . V) . v1 by A19;

then v2 in ((W1, the carrier of S) *graph) . v1 by A2, A50, Def3;

then v2 in Im (W1,v1) by WAYBEL26:def 5;

then ex v19 being object st

( [v19,v2] in W2 & v19 in {v1} ) by RELAT_1:def 13;

hence v in W2 by A55, TARSKI:def 1; :: thesis: verum

end;assume A52: v in V ; :: thesis: v in W2

V in the carrier of (InclPoset (sigma [:S,L:])) ;

then V in sigma [:S,L:] by YELLOW_1:1;

then V c= the carrier of [:S,L:] ;

then V c= [: the carrier of S, the carrier of L:] by YELLOW_3:def 2;

then consider v1, v2 being object such that

A53: v1 in the carrier of S and

A54: v2 in the carrier of L and

A55: v = [v1,v2] by A52, ZFMISC_1:84;

reconsider v2 = v2 as Element of L by A54;

reconsider v1 = v1 as Element of S by A53;

v2 in { y where y is Element of L : [v1,y] in V } by A52, A55;

then v2 in (G . V) . v1 by A19;

then v2 in ((W1, the carrier of S) *graph) . v1 by A2, A50, Def3;

then v2 in Im (W1,v1) by WAYBEL26:def 5;

then ex v19 being object st

( [v19,v2] in W2 & v19 in {v1} ) by RELAT_1:def 13;

hence v in W2 by A55, TARSKI:def 1; :: thesis: verum

proof

then
W = V
by A51, XBOOLE_0:def 10;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in W2 or w in V )

assume A56: w in W2 ; :: thesis: w in V

W1 c= the carrier of [:SS,SL:] ;

then W1 c= [: the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;

then consider w1, w2 being object such that

A57: w1 in the carrier of S and

A58: w2 in the carrier of L and

A59: w = [w1,w2] by A2, A17, A56, ZFMISC_1:84;

reconsider w2 = w2 as Element of L by A58;

reconsider w1 = w1 as Element of S by A57;

w1 in {w1} by TARSKI:def 1;

then w2 in Im (W1,w1) by A56, A59, RELAT_1:def 13;

then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def 5;

then w2 in ((Theta (SS,SL)) . W2) . w1 by A2, Def3;

then w2 in { y where y is Element of L : [w1,y] in V } by A19, A50;

then ex w29 being Element of L st

( w29 = w2 & [w1,w29] in V ) ;

hence w in V by A59; :: thesis: verum

end;assume A56: w in W2 ; :: thesis: w in V

W1 c= the carrier of [:SS,SL:] ;

then W1 c= [: the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;

then consider w1, w2 being object such that

A57: w1 in the carrier of S and

A58: w2 in the carrier of L and

A59: w = [w1,w2] by A2, A17, A56, ZFMISC_1:84;

reconsider w2 = w2 as Element of L by A58;

reconsider w1 = w1 as Element of S by A57;

w1 in {w1} by TARSKI:def 1;

then w2 in Im (W1,w1) by A56, A59, RELAT_1:def 13;

then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def 5;

then w2 in ((Theta (SS,SL)) . W2) . w1 by A2, Def3;

then w2 in { y where y is Element of L : [w1,y] in V } by A19, A50;

then ex w29 being Element of L st

( w29 = w2 & [w1,w29] in V ) ;

hence w in V by A59; :: thesis: verum

hence W in the carrier of (InclPoset (sigma [:S,L:])) ; :: thesis: verum

hence sigma [:S,L:] = the carrier of (InclPoset the topology of [:SS,SL:]) by YELLOW_1:1

.= the topology of [:SS,SL:] by YELLOW_1:1 ;

:: thesis: verum