let L be complete continuous LATTICE; :: thesis:
let T be Scott TopAugmentation of L; :: thesis:
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis:
let f be Function of X,T; :: thesis:
assume A1: f is continuous ; :: thesis:
let Y be non empty TopSpace; :: thesis:
assume A2: X is SubSpace of Y ; :: thesis:
deffunc H₁( set ) -> Element of the carrier of T = "\/" ( { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : $1 in V } ,T);
consider g being Function of the carrier of Y, the carrier of T such that
A3: for x being Element of Y holds g . x = H₁(x) from FUNCT_2:sch 4();
reconsider g = g as Function of Y,T ;
take g ; :: thesis:
A4: dom f = the carrier of X by FUNCT_2:def 1;
A5: for P being Subset of T st P is open holds
g " P is open

let P be Subset of T; :: thesis:
assume P is open ; :: thesis:
then reconsider P = P as open Subset of T ;
for x being set holds
( x in g " P iff ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) )

let x be set ; :: thesis:
thus ( x in g " P implies ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) ) :: thesis:

assume A6: x in g " P ; :: thesis:
then reconsider y = x as Point of Y ;
set A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ;
{ (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } c= the carrier of T

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; :: thesis:
then ex V being open Subset of Y st
( a = inf (f .: (V /\ the carrier of X)) & y in V ) ;
hence a in the carrier of T ; :: thesis:

end;

then reconsider A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } as Subset of T ;
A7: inf (f .: (([#] Y) /\ the carrier of X)) in A ;
A8: A is directed

let a, b be Element of T; :: according to WAYBEL_0:def 1 :: thesis:
assume a in A ; :: thesis:
then consider Va being open Subset of Y such that
A9: a = inf (f .: (Va /\ the carrier of X)) and
A10: y in Va ;
assume b in A ; :: thesis:
then consider Vb being open Subset of Y such that
A11: b = inf (f .: (Vb /\ the carrier of X)) and
A12: y in Vb ;
take inf (f .: ((Va /\ Vb) /\ the carrier of X)) ; :: thesis:
y in Va /\ Vb by A10, A12, XBOOLE_0:def 4;
hence inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A ; :: thesis:
(Va /\ Vb) /\ the carrier of X c= Vb /\ the carrier of X by XBOOLE_1:17, XBOOLE_1:26;
then A13: f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Vb /\ the carrier of X) by RELAT_1:123;
(Va /\ Vb) /\ the carrier of X c= Va /\ the carrier of X by XBOOLE_1:17, XBOOLE_1:26;
then f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Va /\ the carrier of X) by RELAT_1:123;
hence ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) ) by A9, A11, A13, WAYBEL_7:1; :: thesis:

end;

A14: g . y = sup A by A3;
g . y in P by A6, FUNCT_2:38;
then A meets P by A14, A7, A8, WAYBEL11:def 1;
then consider b being object such that
A15: b in A and
A16: b in P by XBOOLE_0:3;
consider B being open Subset of Y such that
A17: b = inf (f .: (B /\ the carrier of X)) and
A18: y in B by A15;
reconsider b = b as Element of T by A17;
take B ; :: thesis:
thus B is open ; :: thesis:
thus B c= g " P :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A19: a in B ; :: thesis:
then reconsider a = a as Point of Y ;
A20: g . a = H₁(a) by A3;
b in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : a in V } by A17, A19;
then b <= g . a by A20, YELLOW_2:22;
then g . a in P by A16, WAYBEL_0:def 20;
hence a in g " P by FUNCT_2:38; :: thesis:

end;

end;

thus ( ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) implies x in g " P ) ; :: thesis:

end;

end;

set gX = g | the carrier of X;
A21: the carrier of X c= the carrier of Y by A2, BORSUK_1:1;
A22: for a being object st a in the carrier of X holds
(g | the carrier of X) . a = f . a

let a be object ; :: thesis:
assume a in the carrier of X ; :: thesis:
then reconsider x = a as Point of X ;
reconsider y = x as Point of Y by A21;
set A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ;
{ (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } c= the carrier of T

end;

then reconsider A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } as Subset of T ;
A23: f . x is_>=_than A

let z be Element of T; :: according to LATTICE3:def 9 :: thesis:
assume z in A ; :: thesis:
then consider V being open Subset of Y such that
A24: z = inf (f .: (V /\ the carrier of X)) and
A25: y in V ;
A26: ex_inf_of f .: (V /\ the carrier of X),T by YELLOW_0:17;
y in V /\ the carrier of X by A25, XBOOLE_0:def 4;
hence z <= f . x by A24, A26, FUNCT_2:35, YELLOW_4:2; :: thesis:

end;

let b be Element of T; :: thesis:
assume A28: for k being Element of T st k in A holds
k <= b ; :: according to LATTICE3:def 9 :: thesis:
A29: for V being open Subset of X st x in V holds
inf (f .: V) <= b

let V be open Subset of X; :: thesis:
V in the topology of X by PRE_TOPC:def 2;
then consider Q being Subset of Y such that
A30: Q in the topology of Y and
A31: V = Q /\ ([#] X) by A2, PRE_TOPC:def 4;
reconsider Q = Q as open Subset of Y by A30, PRE_TOPC:def 2;
assume x in V ; :: thesis:
then y in Q by A31, XBOOLE_0:def 4;
then inf (f .: (Q /\ the carrier of X)) in A ;
hence inf (f .: V) <= b by A28, A31; :: thesis:

end;

end;

end;

thus (g | the carrier of X) . a = g . y by FUNCT_1:49
.= H₁(y) by A3
.= f . a by A23, A27, YELLOW_0:30 ; :: thesis:

end;