let S, T be complete Scott TopLattice; :: thesis: for f being continuous Function of S,T
for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
let f be continuous Function of S,T; :: thesis: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
let N be net of S; :: thesis: f . (lim_inf N) <= lim_inf (f * N)
set x = lim_inf N;
set t = lim_inf (f * N);
A1: [#] T <> {} ;
assume not f . (lim_inf N) <= lim_inf (f * N) ; :: thesis: contradiction
then not f . (lim_inf N) in downarrow (lim_inf (f * N)) by WAYBEL_0:17;
then A2: f . (lim_inf N) in (downarrow (lim_inf (f * N))) ` by XBOOLE_0:def 5;
downarrow (lim_inf (f * N)) is closed by Lm3;
then A3: (downarrow (lim_inf (f * N))) ` is open ;
set U1 = f " ((downarrow (lim_inf (f * N))) ` );
A4: f " ((downarrow (lim_inf (f * N))) ` ) is open by A1, A3, TOPS_2:55;
set D = { ("/\" { (N . k) where k is Element of N : k >= j } ,S) where j is Element of N : verum } ;

now

let f be set ; :: thesis: ( f in { ("/\" { (N . k) where k is Element of N : k >= j } ,S) where j is Element of N : verum } implies f in the carrier of S )
assume f in { ("/\" { (N . k) where k is Element of N : k >= j } ,S) where j is Element of N : verum } ; :: thesis: f in the carrier of S
then consider j being Element of N such that
A5: f = "/\" { (N . k) where k is Element of N : k >= j } ,S ;
thus f in the carrier of S by A5; :: thesis: verum

end;

then reconsider D = { ("/\" { (N . k) where k is Element of N : k >= j } ,S) where j is Element of N : verum } as Subset of S by TARSKI:def 3;
reconsider D = D as non empty directed Subset of S by WAYBEL11:30;
A6: lim_inf N in f " ((downarrow (lim_inf (f * N))) ` ) by A2, FUNCT_2:46;
f " ((downarrow (lim_inf (f * N))) ` ) is property(S) by A4, WAYBEL11:15;
then consider y being Element of S such that
A7: ( y in D & ( for x being Element of S st x in D & x >= y holds
x in f " ((downarrow (lim_inf (f * N))) ` ) ) ) by A6, WAYBEL11:def 3;
consider j being Element of N such that
A8: y = "/\" { (N . k) where k is Element of N : k >= j } ,S by A7;
y <= y ;
then A9: y in f " ((downarrow (lim_inf (f * N))) ` ) by A7;
RelStr(# the carrier of (f * N),the InternalRel of (f * N) #) = RelStr(# the carrier of N,the InternalRel of N #) by WAYBEL_9:def 8;
then reconsider j' = j as Element of (f * N) ;
A10: dom f = the carrier of S by FUNCT_2:def 1;
set fy = "/\" { ((f * N) . k) where k is Element of (f * N) : k >= j' } ,T;
set fD = { ("/\" { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T) where j1 is Element of (f * N) : verum } ;

now

let g be set ; :: thesis: ( g in { ("/\" { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T) where j1 is Element of (f * N) : verum } implies g in the carrier of T )
assume g in { ("/\" { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T) where j1 is Element of (f * N) : verum } ; :: thesis: g in the carrier of T
then consider j being Element of (f * N) such that
A11: g = "/\" { ((f * N) . k) where k is Element of (f * N) : k >= j } ,T ;
thus g in the carrier of T by A11; :: thesis: verum

end;

then reconsider fD = { ("/\" { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T) where j1 is Element of (f * N) : verum } as Subset of T by TARSKI:def 3;
A12: f . y <= "/\" { ((f * N) . k) where k is Element of (f * N) : k >= j' } ,T by A8, Th20;
"/\" { ((f * N) . k) where k is Element of (f * N) : k >= j' } ,T in fD ;
then "/\" { ((f * N) . k) where k is Element of (f * N) : k >= j' } ,T <= sup fD by YELLOW_2:24;
then f . y <= lim_inf (f * N) by A12, ORDERS_2:26;
then f . y in downarrow (lim_inf (f * N)) by WAYBEL_0:17;
then A13: y in f " (downarrow (lim_inf (f * N))) by A10, FUNCT_1:def 13;
f " ((downarrow (lim_inf (f * N))) ` ) = (f " ([#] T)) \ (f " (downarrow (lim_inf (f * N)))) by FUNCT_1:138
.= ([#] S) \ (f " (downarrow (lim_inf (f * N)))) by TOPS_2:52
.= (f " (downarrow (lim_inf (f * N)))) ` ;
then A14: y in (f " ((downarrow (lim_inf (f * N))) ` )) /\ ((f " ((downarrow (lim_inf (f * N))) ` )) ` ) by A9, A13, XBOOLE_0:def 4;
f " ((downarrow (lim_inf (f * N))) ` ) misses (f " ((downarrow (lim_inf (f * N))) ` )) ` by XBOOLE_1:79;
hence contradiction by A14, XBOOLE_0:4; :: thesis: verum