let L be complete LATTICE; :: thesis: ( S7[L] implies S8[L] )
assume A1: S7[L] ; :: thesis: S8[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,) is non empty full SubRelStr of |^ the carrier of L by WAYBEL27:def 4;
then A3: (UPS (L,)) |^ the carrier of S is non empty full SubRelStr of ( |^ the carrier of L) |^ the carrier of S by YELLOW16:39;
UPS (S,(UPS (L,))) is non empty full SubRelStr of (UPS (L,)) |^ the carrier of S by WAYBEL27:def 4;
then A4: UPS (S,(UPS (L,))) is non empty full SubRelStr of ( |^ the carrier of L) |^ the carrier of S by ;
consider f5 being Function of (UPS (L,)),(InclPoset ()) such that
A5: f5 is isomorphic and
A6: for f being directed-sups-preserving Function of L, holds f5 . f = f " {1} by WAYBEL27:33;
set f6 = UPS ((id S),f5);
consider f3 being Function of (UPS (S,(UPS (L,)))),(UPS ([:S,L:],)) 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:],)),(InclPoset (sigma [:S,L:])) such that
A8: f1 is isomorphic and
A9: for f being directed-sups-preserving Function of [:S,L:], holds f1 . f = f " {1} by WAYBEL27:33;
A10: f3 " is isomorphic by ;
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 ()), the InternalRel of (InclPoset ()) #) by YELLOW_9:def 4;
A13: the carrier of (UPS (S,(InclPoset ()))) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))
proof
thus the carrier of (UPS (S,(InclPoset ()))) 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 ())))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UPS (S,(InclPoset ()))) or x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) )
assume A14: x in the carrier of (UPS (S,(InclPoset ()))) ; :: 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 ;
x is directed-sups-preserving Function of S,(InclPoset ()) by ;
then x1 is directed-sups-preserving by ;
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;
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 ()))) )
assume x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ; :: thesis: x in the carrier of (UPS (S,(InclPoset ())))
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 ()) by ;
x1 is directed-sups-preserving by ;
then x2 is directed-sups-preserving by ;
hence x in the carrier of (UPS (S,(InclPoset ()))) by ; :: thesis: verum
end;
then reconsider G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ") as Function of (InclPoset (sigma [:S,L:])),(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 ) |^ the carrier of [:S,L:] = |^ [: the carrier of S, the carrier of L:] & UPS ([:S,L:],) is non empty full SubRelStr of |^ the carrier of [:S,L:] ) by ;
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
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,)) by WAYBEL27:def 4;
reconsider f2V = (f1 ") . V as directed-sups-preserving Function of [:S,L:], by WAYBEL27:def 4;
A20: ( f5 is sups-preserving & (f5 * fff) * (id the carrier of S) = f5 * fff ) by ;
A21: ((f3 ") . ((f1 ") . V)) . s is directed-sups-preserving Function of L, 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 ;
then A23: (G . V) . s = f5 . (fff . s) by FUNCT_2:15
.= (((f3 ") . ((f1 ") . V)) . s) " {1} by ;
A24: rng f1 = [#] (InclPoset (sigma [:S,L:])) by ;
dom (f3 ") = the carrier of (UPS ([:S,L:],)) 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 ;
then A26: V = (id (rng f1)) . V
.= (f1 * (f1 ")) . V by
.= 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 (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 ;
then reconsider y = x as Element of L by ;
(((f3 ") . ((f1 ") . V)) . s) . x in {1} by ;
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 ;
then ((f1 ") . V) . (s,y) in {1} by TARSKI:def 1;
then [s,y] in ((f1 ") . V) " {1} by ;
hence x in { y where y is Element of L : [s,y] in V } by A26; :: thesis: verum
end;
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 )
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 ;
then ((f1 ") . V) . (s,y) = 1 by TARSKI:def 1;
then cs . y = 1 by ;
then (((f3 ") . ((f1 ") . V)) . s) . y in {1} by ;
hence x in (G . V) . s by ; :: thesis: verum
end;
S6[SL] by A1, A11, Lm8;
then S4[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:])
proof
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 ;
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 ;
then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;
A37: V1 c= W1
proof
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 ;
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 ;
then v2 in (G . V1) . v1 by A19;
then v2 in ((W1, the carrier of S) *graph) . v1 by ;
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 ; :: thesis: verum
end;
W2 c= V1
proof
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 ;
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 ;
then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def 5;
then w2 in ((Theta (SS,SL)) . W2) . w1 by ;
then w2 in { y where y is Element of L : [w1,y] in V1 } by ;
then ex w29 being Element of L st
( w29 = w2 & [w1,w29] in V1 ) ;
hence w in V1 by A45; :: thesis: verum
end;
then W2 = V by ;
hence V in the carrier of (InclPoset the topology of [:SS,SL:]) ; :: thesis: verum
end;
InclPoset () = InclPoset the topology of SL by YELLOW_9:51;
then UPS ((id S),f5) is isomorphic by ;
then A46: (UPS ((id S),f5)) * (f3 ") is isomorphic by ;
A47: f1 " is isomorphic by ;
the carrier of (InclPoset the topology of [:SS,SL:]) c= the carrier of (InclPoset (sigma [:S,L:]))
proof
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 ;
then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;
G is onto by ;
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
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 ;
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 ;
then v2 in (G . V) . v1 by A19;
then v2 in ((W1, the carrier of S) *graph) . v1 by ;
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 ; :: thesis: verum
end;
W2 c= V
proof
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 ;
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 ;
then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def 5;
then w2 in ((Theta (SS,SL)) . W2) . w1 by ;
then w2 in { y where y is Element of L : [w1,y] in V } by ;
then ex w29 being Element of L st
( w29 = w2 & [w1,w29] in V ) ;
hence w in V by A59; :: thesis: verum
end;
then W = V by ;
hence W in the carrier of (InclPoset (sigma [:S,L:])) ; :: thesis: verum
end;
then the carrier of (InclPoset (sigma [:S,L:])) = the carrier of (InclPoset the topology of [:SS,SL:]) by A34;
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