:: WAYBEL21 semantic presentation

begin

definition
let S, T be Semilattice;
assume B1: ( S is upper-bounded implies T is upper-bounded ) ;
mode SemilatticeHomomorphism of S,T ->  Function of S,T means :Def1: :: WAYBEL21:def 1
 for X being finite Subset of S holds it preserves_inf_of X;
existence
 ex b1 being Function of S,T st
for X being finite Subset of S holds b1 preserves_inf_of X
proof
reconsider f = the carrier of S --> (Top T) as Function of S,T ;
take  f ; ::_thesis: for X being finite Subset of S holds f preserves_inf_of X
let X be finite Subset of S; ::_thesis: f preserves_inf_of X
assume A1: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
percases ( X = {} or X <> {} ) ;
supposeA2: X = {} ; ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
then A3: f .: X = {} ;
hence  ex_inf_of f .: X,T by B1, A1, A2, WAYBEL20:5, YELLOW_0:43; ::_thesis: "/\" ((f .: X),T) = f . ("/\" (X,S))
thus  f . (inf X) = inf (f .: X) by A3, FUNCOP_1:7; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
then reconsider A = X as non empty Subset of S ;
set a = the Element of A;
reconsider a = the Element of A as Element of S ;
A4: dom f = the carrier of S by FUNCOP_1:13;
 f . a = Top T by FUNCOP_1:7;
then  Top T in f .: X by A4, FUNCT_1:def_6;
then A5: {(Top T)} c= f .: X by ZFMISC_1:31;
 f .: X c= {(Top T)} by FUNCOP_1:81;
then A6: {(Top T)} = f .: X by A5, XBOOLE_0:def_10;
 f . (inf X) = Top T by FUNCOP_1:7;
hence  ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) by A6, YELLOW_0:38, YELLOW_0:39; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def_1_:_
 for S, T being Semilattice st ( S is upper-bounded implies T is upper-bounded ) holds
for b3 being Function of S,T holds
( b3 is SemilatticeHomomorphism of S,T iff for X being finite Subset of S holds b3 preserves_inf_of X );

registration
let S, T be Semilattice;
cluster Function-like V29( the carrier of S, the carrier of T) meet-preserving  ->  monotone for Element of K22(K23( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is meet-preserving holds
b1 is monotone
proof
let f be Function of S,T; ::_thesis: ( f is meet-preserving implies f is monotone )
assume A1: f is meet-preserving ; ::_thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y )
assume  x <= y ; ::_thesis: f . x <= f . y
then  x = x "/\" y by YELLOW_0:25;
then  f . x = (f . x) "/\" (f . y) by A1, WAYBEL_6:1;
hence  f . x <= f . y by YELLOW_0:25; ::_thesis: verum
end;
end;

registration
let S be Semilattice;
let T be upper-bounded Semilattice;
cluster  ->  meet-preserving for SemilatticeHomomorphism of S,T;
coherence
 for b1 being SemilatticeHomomorphism of S,T holds b1 is meet-preserving
proof
let f be SemilatticeHomomorphism of S,T; ::_thesis: f is meet-preserving
let x, y be Element of S; :: according to WAYBEL_0:def_34 ::_thesis: f preserves_inf_of {x,y}
thus  f preserves_inf_of {x,y} by Def1; ::_thesis: verum
end;
end;

theorem :: WAYBEL21:1
for S, T being upper-bounded Semilattice
for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T
proof
let S, T be upper-bounded Semilattice; ::_thesis: for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T
let f be SemilatticeHomomorphism of S,T; ::_thesis: f . (Top S) = Top T
A1: f preserves_inf_of {} S by Def1;
 ex_inf_of {} S,S by YELLOW_0:43;
then  f . (inf ({} S)) = inf (f .: ({} S)) by A1, WAYBEL_0:def_30;
hence  f . (Top S) = Top T ; ::_thesis: verum
end;

theorem Th2: :: WAYBEL21:2
for S, T being Semilattice
for f being Function of S,T st f is meet-preserving holds
for X being non empty finite Subset of S holds f preserves_inf_of X
proof
let S, T be Semilattice; ::_thesis: for f being Function of S,T st f is meet-preserving holds
for X being non empty finite Subset of S holds f preserves_inf_of X
let f be Function of S,T; ::_thesis: ( f is meet-preserving implies for X being non empty finite Subset of S holds f preserves_inf_of X )
assume A1: f is meet-preserving ; ::_thesis: for X being non empty finite Subset of S holds f preserves_inf_of X
let X be non empty finite Subset of S; ::_thesis: f preserves_inf_of X
assume  ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
A2: X is finite ;
defpred S1[ set ] means ( $1 <> {} implies ( ex_inf_of $1,S & ex_inf_of f .: $1,T & inf (f .: $1) = f . ("/\" ($1,S)) ) );
A3: S1[ {} ] ;
A4: now__::_thesis:_for_y,_x_being_set_st_y_in_X_&_x_c=_X_&_S1[x]_holds_
S1[x_\/_{y}]
let y, x be set ; ::_thesis: ( y in X & x c= X & S1[x] implies S1[x \/ {y}] )
assume that
A5: y in X and
 x c= X and
A6: S1[x] ; ::_thesis: S1[x \/ {y}]
thus  S1[x \/ {y}] ::_thesis: verum
proof
assume  x \/ {y} <> {} ; ::_thesis: ( ex_inf_of x \/ {y},S & ex_inf_of f .: (x \/ {y}),T & inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) )
reconsider y9 = y as Element of S by A5;
set fy = f . y9;
A7: ex_inf_of {(f . y9)},T by YELLOW_0:38;
A8: inf {(f . y9)} = f . y9 by YELLOW_0:39;
A9: ex_inf_of {y9},S by YELLOW_0:38;
A10: inf {y9} = y by YELLOW_0:39;
thus  ex_inf_of x \/ {y},S by A6, A9, YELLOW_2:4; ::_thesis: ( ex_inf_of f .: (x \/ {y}),T & inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) )
 dom f = the carrier of S by FUNCT_2:def_1;
then A11: Im (f,y) = {(f . y9)} by FUNCT_1:59;
then A12: f .: (x \/ {y}) = (f .: x) \/ {(f . y9)} by RELAT_1:120;
hence  ex_inf_of f .: (x \/ {y}),T by A6, A7, A11, YELLOW_2:4; ::_thesis: inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S))
percases ( x = {} or x <> {} ) ;
suppose x = {} ; ::_thesis: inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S))
hence  inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) by A8, A11, YELLOW_0:39; ::_thesis: verum
end;
supposeA13: x <> {} ; ::_thesis: inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S))
hence  "/\" ((f .: (x \/ {y})),T) = (f . ("/\" (x,S))) "/\" (f . y9) by A6, A7, A8, A12, YELLOW_2:4
.= f . (("/\" (x,S)) "/\" y9) by A1, WAYBEL_6:1
.= f . ("/\" ((x \/ {y}),S)) by A6, A9, A10, A13, YELLOW_2:4 ;
::_thesis: verum
end;
end;
end;
end;
 S1[X] from FINSET_1:sch_2(A2, A3, A4);
hence  ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) ; ::_thesis: verum
end;

theorem :: WAYBEL21:3
for S, T being upper-bounded Semilattice
for f being meet-preserving Function of S,T st f . (Top S) = Top T holds
f is SemilatticeHomomorphism of S,T
proof
let S, T be upper-bounded Semilattice; ::_thesis: for f being meet-preserving Function of S,T st f . (Top S) = Top T holds
f is SemilatticeHomomorphism of S,T
let f be meet-preserving Function of S,T; ::_thesis: ( f . (Top S) = Top T implies f is SemilatticeHomomorphism of S,T )
assume A1: f . (Top S) = Top T ; ::_thesis: f is SemilatticeHomomorphism of S,T
thus  ( S is upper-bounded implies T is upper-bounded ) ; :: according to WAYBEL21:def_1 ::_thesis: for X being finite Subset of S holds f preserves_inf_of X
let X be finite Subset of S; ::_thesis: f preserves_inf_of X
A2: ex_inf_of f .: {},T by YELLOW_0:43;
 ( X = {} or f preserves_inf_of X ) by Th2;
hence  f preserves_inf_of X by A1, A2, WAYBEL_0:def_30; ::_thesis: verum
end;

theorem Th4: :: WAYBEL21:4
for S, T being Semilattice
for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
for X being non empty Subset of S holds f preserves_inf_of X
proof
let S, T be Semilattice; ::_thesis: for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
for X being non empty Subset of S holds f preserves_inf_of X
let f be Function of S,T; ::_thesis: ( f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) implies for X being non empty Subset of S holds f preserves_inf_of X )
assume that
A1: f is meet-preserving and
A2: for X being non empty filtered Subset of S holds f preserves_inf_of X ; ::_thesis: for X being non empty Subset of S holds f preserves_inf_of X
let X be non empty Subset of S; ::_thesis: f preserves_inf_of X
assume A3: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
defpred S1[ set ] means  ex Y being non empty finite Subset of X st
( ex_inf_of Y,S & $1 = "/\" (Y,S) );
consider Z being set  such that
A4: for x being set holds
( x in Z iff ( x in the carrier of S & S1[x] ) ) from XBOOLE_0:sch_1();
set a = the Element of X;
reconsider a9 = the Element of X as Element of S ;
A5: ex_inf_of { the Element of X},S by YELLOW_0:38;
A6: inf {a9} = the Element of X by YELLOW_0:39;
 Z c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in the carrier of S )
thus  ( not x in Z or x in the carrier of S ) by A4; ::_thesis: verum
end;
then reconsider Z = Z as non empty Subset of S by A4, A5, A6;
A7: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_inf_of_Y,S
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,S )
 Y is Subset of S by XBOOLE_1:1;
hence  ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; ::_thesis: verum
end;
A8: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"/\"_(Y,S)_in_Z
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,S) in Z )
reconsider Y9 = Y as Subset of S by XBOOLE_1:1;
assume A9: Y <> {} ; ::_thesis: "/\" (Y,S) in Z
then  ex_inf_of Y9,S by YELLOW_0:55;
hence  "/\" (Y,S) in Z by A4, A9; ::_thesis: verum
end;
A10: now__::_thesis:_for_x_being_Element_of_S_st_x_in_Z_holds_
ex_Y_being_finite_Subset_of_X_st_
(_ex_inf_of_Y,S_&_x_=_"/\"_(Y,S)_)
let x be Element of S; ::_thesis: ( x in Z implies ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" (Y,S) ) )
assume  x in Z ; ::_thesis: ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" (Y,S) )
then  ex Y being non empty finite Subset of X st
( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4;
hence  ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" (Y,S) ) ; ::_thesis: verum
end;
then A11: Z is filtered by A7, A8, WAYBEL_0:56;
A12: ex_inf_of Z,S by A3, A7, A8, A10, WAYBEL_0:58;
A13: f preserves_inf_of Z by A2, A11;
then A14: ex_inf_of f .: Z,T by A12, WAYBEL_0:def_30;
A15: inf (f .: Z) = f . (inf Z) by A12, A13, WAYBEL_0:def_30;
A16: inf Z = inf X by A3, A7, A8, A10, WAYBEL_0:59;
 X c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume A17: x in X ; ::_thesis: x in Z
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;
reconsider x = x as Element of S by A17;
 Y is Subset of S by XBOOLE_1:1;
then A18: ex_inf_of Y,S by YELLOW_0:55;
 x = "/\" (Y,S) by YELLOW_0:39;
hence  x in Z by A4, A18; ::_thesis: verum
end;
then A19: f .: X c= f .: Z by RELAT_1:123;
A20: f .: Z is_>=_than f . (inf X) by A14, A15, A16, YELLOW_0:31;
A21: f .: X is_>=_than f . (inf X)
proof
let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or f . (inf X) <= x )
assume  x in f .: X ; ::_thesis: f . (inf X) <= x
hence  f . (inf X) <= x by A19, A20, LATTICE3:def_8; ::_thesis: verum
end;
A22: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_>=_than_b_holds_
f_._(inf_X)_>=_b
let b be Element of T; ::_thesis: ( f .: X is_>=_than b implies f . (inf X) >= b )
assume A23: f .: X is_>=_than b ; ::_thesis: f . (inf X) >= b
 f .: Z is_>=_than b
proof
let a be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not a in f .: Z or b <= a )
assume  a in f .: Z ; ::_thesis: b <= a
then consider x being set  such that
 x in dom f and
A24: x in Z and
A25: a = f . x by FUNCT_1:def_6;
consider Y being non empty finite Subset of X such that
A26: ex_inf_of Y,S and
A27: x = "/\" (Y,S) by A4, A24;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
A28: f .: Y c= f .: X by RELAT_1:123;
A29: f preserves_inf_of Y by A1, Th2;
A30: b is_<=_than f .: Y by A23, A28, YELLOW_0:9;
A31: a = "/\" ((f .: Y),T) by A25, A26, A27, A29, WAYBEL_0:def_30;
 ex_inf_of f .: Y,T by A26, A29, WAYBEL_0:def_30;
hence  b <= a by A30, A31, YELLOW_0:def_10; ::_thesis: verum
end;
hence  f . (inf X) >= b by A14, A15, A16, YELLOW_0:31; ::_thesis: verum
end;
hence  ex_inf_of f .: X,T by A21, YELLOW_0:16; ::_thesis: "/\" ((f .: X),T) = f . ("/\" (X,S))
hence  inf (f .: X) = f . (inf X) by A21, A22, YELLOW_0:def_10; ::_thesis: verum
end;

theorem Th5: :: WAYBEL21:5
for S, T being Semilattice
for f being Function of S,T st f is infs-preserving holds
f is SemilatticeHomomorphism of S,T
proof
let S, T be Semilattice; ::_thesis: for f being Function of S,T st f is infs-preserving holds
f is SemilatticeHomomorphism of S,T
let f be Function of S,T; ::_thesis: ( f is infs-preserving implies f is SemilatticeHomomorphism of S,T )
assume A1: f is infs-preserving ; ::_thesis: f is SemilatticeHomomorphism of S,T
reconsider e = {} as Subset of S by XBOOLE_1:2;
hereby  :: according to WAYBEL21:def_1 ::_thesis: for X being finite Subset of S holds f preserves_inf_of X
assume  S is upper-bounded ; ::_thesis: T is upper-bounded
then A2: ex_inf_of e,S by YELLOW_0:43;
 f preserves_inf_of e by A1, WAYBEL_0:def_32;
then A3: ex_inf_of f .: e,T by A2, WAYBEL_0:def_30;
 f .: e = {} ;
hence  T is upper-bounded by A3, WAYBEL20:5; ::_thesis: verum
end;
let X be finite Subset of S; ::_thesis: f preserves_inf_of X
thus  f preserves_inf_of X by A1, WAYBEL_0:def_32; ::_thesis: verum
end;

theorem Th6: :: WAYBEL21:6
for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
proof
let S1, T1, S2, T2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) )
assume that
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
let f1 be Function of S1,T1; ::_thesis: for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
let f2 be Function of S2,T2; ::_thesis: ( f1 = f2 implies ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) )
assume A3: f1 = f2 ; ::_thesis: ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
thus  ( f1 is infs-preserving implies f2 is infs-preserving ) ::_thesis: ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving )
proof
assume A4: for X being Subset of S1 holds f1 preserves_inf_of X ; :: according to WAYBEL_0:def_32 ::_thesis: f2 is infs-preserving
let X be Subset of S2; :: according to WAYBEL_0:def_32 ::_thesis: f2 preserves_inf_of X
thus  f2 preserves_inf_of X by A1, A2, A3, A4, WAYBEL_0:65; ::_thesis: verum
end;
assume A5: for X being Subset of S1 st not X is empty & X is directed holds
f1 preserves_sup_of X ; :: according to WAYBEL_0:def_37 ::_thesis: f2 is directed-sups-preserving
let X be Subset of S2; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or f2 preserves_sup_of X )
reconsider Y = X as Subset of S1 by A1;
assume  ( not X is empty & X is directed ) ; ::_thesis: f2 preserves_sup_of X
then  f1 preserves_sup_of Y by A1, A5, WAYBEL_0:3;
hence  f2 preserves_sup_of X by A1, A2, A3, WAYBEL_0:65; ::_thesis: verum
end;

theorem :: WAYBEL21:7
for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
proof
let S1, T1, S2, T2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) )
assume that
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
let f1 be Function of S1,T1; ::_thesis: for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
let f2 be Function of S2,T2; ::_thesis: ( f1 = f2 implies ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) )
assume A3: f1 = f2 ; ::_thesis: ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
thus  ( f1 is sups-preserving implies f2 is sups-preserving ) ::_thesis: ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving )
proof
assume A4: for X being Subset of S1 holds f1 preserves_sup_of X ; :: according to WAYBEL_0:def_33 ::_thesis: f2 is sups-preserving
let X be Subset of S2; :: according to WAYBEL_0:def_33 ::_thesis: f2 preserves_sup_of X
thus  f2 preserves_sup_of X by A1, A2, A3, A4, WAYBEL_0:65; ::_thesis: verum
end;
assume A5: for X being Subset of S1 st not X is empty & X is filtered holds
f1 preserves_inf_of X ; :: according to WAYBEL_0:def_36 ::_thesis: f2 is filtered-infs-preserving
let X be Subset of S2; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or f2 preserves_inf_of X )
reconsider Y = X as Subset of S1 by A1;
assume  ( not X is empty & X is filtered ) ; ::_thesis: f2 preserves_inf_of X
then  f1 preserves_inf_of Y by A1, A5, WAYBEL_0:4;
hence  f2 preserves_inf_of X by A1, A2, A3, WAYBEL_0:65; ::_thesis: verum
end;

theorem Th8: :: WAYBEL21:8
for T being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving
proof
let T be complete LATTICE; ::_thesis: for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving
let S be non empty full infs-inheriting SubRelStr of T; ::_thesis: incl (S,T) is infs-preserving
set f = incl (S,T);
let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: incl (S,T) preserves_inf_of X
assume  ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (incl (S,T)) .: X,T & "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) )
thus  ex_inf_of (incl (S,T)) .: X,T by YELLOW_0:17; ::_thesis: "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S))
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then A1: incl (S,T) = id the carrier of S by YELLOW_9:def_1;
then A2: (incl (S,T)) .: X = X by FUNCT_1:92;
A3: ex_inf_of X,T by YELLOW_0:17;
A4: (incl (S,T)) . (inf X) = inf X by A1, FUNCT_1:18;
 "/\" (X,T) in the carrier of S by A3, YELLOW_0:def_18;
hence  "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) by A2, A3, A4, YELLOW_0:63; ::_thesis: verum
end;

theorem :: WAYBEL21:9
for T being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of T holds incl (S,T) is sups-preserving
proof
let T be complete LATTICE; ::_thesis: for S being non empty full sups-inheriting SubRelStr of T holds incl (S,T) is sups-preserving
let S be non empty full sups-inheriting SubRelStr of T; ::_thesis: incl (S,T) is sups-preserving
set f = incl (S,T);
let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: incl (S,T) preserves_sup_of X
assume  ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (incl (S,T)) .: X,T & "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) )
thus  ex_sup_of (incl (S,T)) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S))
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then A1: incl (S,T) = id the carrier of S by YELLOW_9:def_1;
then A2: (incl (S,T)) .: X = X by FUNCT_1:92;
A3: ex_sup_of X,T by YELLOW_0:17;
A4: (incl (S,T)) . (sup X) = sup X by A1, FUNCT_1:18;
 "\/" (X,T) in the carrier of S by A3, YELLOW_0:def_19;
hence  "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) by A2, A3, A4, YELLOW_0:64; ::_thesis: verum
end;

theorem Th10: :: WAYBEL21:10
for T being non empty up-complete Poset
for S being non empty full directed-sups-inheriting SubRelStr of T holds incl (S,T) is directed-sups-preserving
proof
let T be non empty up-complete Poset; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of T holds incl (S,T) is directed-sups-preserving
let S be non empty full directed-sups-inheriting SubRelStr of T; ::_thesis: incl (S,T) is directed-sups-preserving
set f = incl (S,T);
let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or incl (S,T) preserves_sup_of X )
assume that
A1: ( not X is empty & X is directed ) and
 ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (incl (S,T)) .: X,T & "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) )
reconsider X9 = X as non empty directed Subset of T by A1, YELLOW_2:7;
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then A2: incl (S,T) = id the carrier of S by YELLOW_9:def_1;
then A3: (incl (S,T)) .: X = X9 by FUNCT_1:92;
A4: (incl (S,T)) . (sup X) = sup X by A2, FUNCT_1:18;
thus  ex_sup_of (incl (S,T)) .: X,T by A3, WAYBEL_0:75; ::_thesis: "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S))
hence  "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) by A1, A3, A4, WAYBEL_0:7; ::_thesis: verum
end;

theorem :: WAYBEL21:11
for T being complete LATTICE
for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving
proof
let T be complete LATTICE; ::_thesis: for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving
let S be non empty full filtered-infs-inheriting SubRelStr of T; ::_thesis: incl (S,T) is filtered-infs-preserving
set f = incl (S,T);
let X be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or incl (S,T) preserves_inf_of X )
assume that
A1: ( not X is empty & X is filtered ) and
 ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (incl (S,T)) .: X,T & "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) )
thus  ex_inf_of (incl (S,T)) .: X,T by YELLOW_0:17; ::_thesis: "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S))
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then A2: incl (S,T) = id the carrier of S by YELLOW_9:def_1;
then A3: (incl (S,T)) .: X = X by FUNCT_1:92;
A4: ex_inf_of X,T by YELLOW_0:17;
 (incl (S,T)) . (inf X) = inf X by A2, FUNCT_1:18;
hence  "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) by A1, A3, A4, WAYBEL_0:6; ::_thesis: verum
end;

theorem Th12: :: WAYBEL21:12
for T1, T2, R being RelStr
for S being SubRelStr of T1 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds
( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )
proof
let T, T2, R be RelStr ; ::_thesis: for S being SubRelStr of T st RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds
( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )
let S be SubRelStr of T; ::_thesis: ( RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) implies ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) ) )
assume that
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) and
A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) ; ::_thesis: ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )
A3: the carrier of R c= the carrier of T2 by A1, A2, YELLOW_0:def_13;
A4: the InternalRel of R c= the InternalRel of T2 by A1, A2, YELLOW_0:def_13;
hence  R is SubRelStr of T2 by A3, YELLOW_0:def_13; ::_thesis: ( S is full implies R is full SubRelStr of T2 )
assume  the InternalRel of S = the InternalRel of T |_2 the carrier of S ; :: according to YELLOW_0:def_14 ::_thesis: R is full SubRelStr of T2
hence  R is full SubRelStr of T2 by A1, A2, A3, A4, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;

theorem Th13: :: WAYBEL21:13
for T being non empty RelStr holds T is full infs-inheriting sups-inheriting SubRelStr of T
proof
let T be non empty RelStr ; ::_thesis: T is full infs-inheriting sups-inheriting SubRelStr of T
reconsider R = T as full SubRelStr of T by YELLOW_6:6;
A1: R is infs-inheriting
proof
let X be Subset of R; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,T or "/\" (X,T) in the carrier of R )
thus  ( not ex_inf_of X,T or "/\" (X,T) in the carrier of R ) ; ::_thesis: verum
end;
 R is sups-inheriting
proof
let X be Subset of R; :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,T or "\/" (X,T) in the carrier of R )
thus  ( not ex_sup_of X,T or "\/" (X,T) in the carrier of R ) ; ::_thesis: verum
end;
hence  T is full infs-inheriting sups-inheriting SubRelStr of T by A1; ::_thesis: verum
end;

registration
let T be complete LATTICE;
cluster non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting with_infima complete for SubRelStr of T;
existence
 ex b1 being CLSubFrame of T st b1 is complete
proof
 T is full infs-inheriting sups-inheriting SubRelStr of T by Th13;
hence  ex b1 being CLSubFrame of T st b1 is complete ; ::_thesis: verum
end;
end;

theorem Th14: :: WAYBEL21:14
for T being Semilattice
for S being non empty full SubRelStr of T holds
( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )
proof
let T be Semilattice; ::_thesis: for S being non empty full SubRelStr of T holds
( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )
let S be non empty full SubRelStr of T; ::_thesis: ( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )
hereby  ::_thesis: ( ( for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ) implies S is meet-inheriting )
assume A1: S is meet-inheriting ; ::_thesis: for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S
let X be non empty finite Subset of S; ::_thesis: "/\" (X,T) in the carrier of S
A2: X is finite ;
defpred S1[ set ] means ( $1 <> {} implies "/\" ($1,T) in the carrier of S );
A3: S1[ {} ] ;
A4: now__::_thesis:_for_y,_x_being_set_st_y_in_X_&_x_c=_X_&_S1[x]_holds_
S1[x_\/_{y}]
let y, x be set ; ::_thesis: ( y in X & x c= X & S1[x] implies S1[x \/ {y}] )
assume that
A5: y in X and
A6: x c= X and
A7: S1[x] ; ::_thesis: S1[x \/ {y}]
thus  S1[x \/ {y}] ::_thesis: verum
proof
assume  x \/ {y} <> {} ; ::_thesis: "/\" ((x \/ {y}),T) in the carrier of S
reconsider y9 = y as Element of S by A5;
reconsider z = y9 as Element of T by YELLOW_0:58;
A8: x c= the carrier of S by A6, XBOOLE_1:1;
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1:1;
A9: ex_inf_of {z},T by YELLOW_0:38;
A10: inf {z} = y9 by YELLOW_0:39;
now__::_thesis:_(_x9_<>_{}_implies_inf_(x9_\/_{z})_in_the_carrier_of_S_)
assume A11: x9 <> {} ; ::_thesis: inf (x9 \/ {z}) in the carrier of S
then  ex_inf_of x9,T by YELLOW_0:55;
then A12: inf (x9 \/ {z}) = (inf x9) "/\" z by A9, A10, YELLOW_2:4;
 ex_inf_of {(inf x9),z},T by YELLOW_0:21;
then  inf {(inf x9),z} in the carrier of S by A1, A7, A11, YELLOW_0:def_16;
hence  inf (x9 \/ {z}) in the carrier of S by A12, YELLOW_0:40; ::_thesis: verum
end;
hence  "/\" ((x \/ {y}),T) in the carrier of S by A10; ::_thesis: verum
end;
end;
 S1[X] from FINSET_1:sch_2(A2, A3, A4);
hence  "/\" (X,T) in the carrier of S ; ::_thesis: verum
end;
assume A13: for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ; ::_thesis: S is meet-inheriting
let x, y be Element of T; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S )
assume that
A14: x in the carrier of S and
A15: y in the carrier of S ; ::_thesis: ( not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S )
 {x,y} c= the carrier of S by A14, A15, ZFMISC_1:32;
hence  ( not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S ) by A13; ::_thesis: verum
end;

theorem Th15: :: WAYBEL21:15
for T being sup-Semilattice
for S being non empty full SubRelStr of T holds
( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )
proof
let T be sup-Semilattice; ::_thesis: for S being non empty full SubRelStr of T holds
( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )
let S be non empty full SubRelStr of T; ::_thesis: ( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )
hereby  ::_thesis: ( ( for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ) implies S is join-inheriting )
assume A1: S is join-inheriting ; ::_thesis: for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S
let X be non empty finite Subset of S; ::_thesis: "\/" (X,T) in the carrier of S
A2: X is finite ;
defpred S1[ set ] means ( $1 <> {} implies "\/" ($1,T) in the carrier of S );
A3: S1[ {} ] ;
A4: now__::_thesis:_for_y,_x_being_set_st_y_in_X_&_x_c=_X_&_S1[x]_holds_
S1[x_\/_{y}]
let y, x be set ; ::_thesis: ( y in X & x c= X & S1[x] implies S1[x \/ {y}] )
assume that
A5: y in X and
A6: x c= X and
A7: S1[x] ; ::_thesis: S1[x \/ {y}]
reconsider y9 = y as Element of S by A5;
reconsider z = y9 as Element of T by YELLOW_0:58;
thus  S1[x \/ {y}] ::_thesis: verum
proof
assume  x \/ {y} <> {} ; ::_thesis: "\/" ((x \/ {y}),T) in the carrier of S
A8: x c= the carrier of S by A6, XBOOLE_1:1;
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1:1;
A9: ex_sup_of {z},T by YELLOW_0:38;
A10: sup {z} = y9 by YELLOW_0:39;
now__::_thesis:_(_x9_<>_{}_implies_sup_(x9_\/_{z})_in_the_carrier_of_S_)
assume A11: x9 <> {} ; ::_thesis: sup (x9 \/ {z}) in the carrier of S
then  ex_sup_of x9,T by YELLOW_0:54;
then A12: sup (x9 \/ {z}) = (sup x9) "\/" z by A9, A10, YELLOW_2:3;
 ex_sup_of {(sup x9),z},T by YELLOW_0:20;
then  sup {(sup x9),z} in the carrier of S by A1, A7, A11, YELLOW_0:def_17;
hence  sup (x9 \/ {z}) in the carrier of S by A12, YELLOW_0:41; ::_thesis: verum
end;
hence  "\/" ((x \/ {y}),T) in the carrier of S by A10; ::_thesis: verum
end;
end;
 S1[X] from FINSET_1:sch_2(A2, A3, A4);
hence  "\/" (X,T) in the carrier of S ; ::_thesis: verum
end;
assume A13: for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ; ::_thesis: S is join-inheriting
let x, y be Element of T; :: according to YELLOW_0:def_17 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S )
assume that
A14: x in the carrier of S and
A15: y in the carrier of S ; ::_thesis: ( not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S )
 {x,y} c= the carrier of S by A14, A15, ZFMISC_1:32;
hence  ( not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S ) by A13; ::_thesis: verum
end;

theorem Th16: :: WAYBEL21:16
for T being upper-bounded Semilattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds
S is infs-inheriting
proof
let T be upper-bounded Semilattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds
S is infs-inheriting
let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: ( Top T in the carrier of S & S is filtered-infs-inheriting implies S is infs-inheriting )
assume that
A1: Top T in the carrier of S and
A2: S is filtered-infs-inheriting ; ::_thesis: S is infs-inheriting
let A be Subset of S; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of A,T or "/\" (A,T) in the carrier of S )
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then reconsider C = A as Subset of T by XBOOLE_1:1;
set F = fininfs C;
assume A3: ex_inf_of A,T ; ::_thesis: "/\" (A,T) in the carrier of S
then A4: inf (fininfs C) = inf C by WAYBEL_0:60;
 fininfs C c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in fininfs C or x in the carrier of S )
assume  x in fininfs C ; ::_thesis: x in the carrier of S
then consider Y being finite Subset of C such that
A5: x = "/\" (Y,T) and
 ex_inf_of Y,T ;
reconsider Y = Y as finite Subset of T by XBOOLE_1:1;
reconsider Z = Y as finite Subset of S by XBOOLE_1:1;
assume A6: not x in the carrier of S ; ::_thesis: contradiction
then  Z <> {} by A1, A5;
hence  contradiction by A5, A6, Th14; ::_thesis: verum
end;
then reconsider G = fininfs C as non empty Subset of S ;
reconsider G = G as non empty filtered Subset of S by WAYBEL10:23;
A7: now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_
ex_inf_of_Y,T
let Y be finite Subset of C; ::_thesis: ( Y <> {} implies ex_inf_of Y,T )
 Y c= the carrier of T by XBOOLE_1:1;
hence  ( Y <> {} implies ex_inf_of Y,T ) by YELLOW_0:55; ::_thesis: verum
end;
A8: now__::_thesis:_for_x_being_Element_of_T_st_x_in_fininfs_C_holds_
ex_Y_being_finite_Subset_of_C_st_
(_ex_inf_of_Y,T_&_x_=_"/\"_(Y,T)_)
let x be Element of T; ::_thesis: ( x in fininfs C implies ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) ) )
assume  x in fininfs C ; ::_thesis: ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) )
then  ex Y being finite Subset of C st
( x = "/\" (Y,T) & ex_inf_of Y,T ) ;
hence  ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) ) ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_
"/\"_(Y,T)_in_fininfs_C
let Y be finite Subset of C; ::_thesis: ( Y <> {} implies "/\" (Y,T) in fininfs C )
reconsider Z = Y as finite Subset of T by XBOOLE_1:1;
assume  Y <> {} ; ::_thesis: "/\" (Y,T) in fininfs C
then  ex_inf_of Z,T by YELLOW_0:55;
hence  "/\" (Y,T) in fininfs C ; ::_thesis: verum
end;
then  ex_inf_of G,T by A3, A7, A8, WAYBEL_0:58;
hence  "/\" (A,T) in the carrier of S by A2, A4, WAYBEL_0:def_3; ::_thesis: verum
end;

theorem :: WAYBEL21:17
for T being lower-bounded sup-Semilattice
for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds
S is sups-inheriting
proof
let T be lower-bounded sup-Semilattice; ::_thesis: for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds
S is sups-inheriting
let S be non empty full join-inheriting SubRelStr of T; ::_thesis: ( Bottom T in the carrier of S & S is directed-sups-inheriting implies S is sups-inheriting )
assume that
A1: Bottom T in the carrier of S and
A2: S is directed-sups-inheriting ; ::_thesis: S is sups-inheriting
let A be Subset of S; :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of A,T or "\/" (A,T) in the carrier of S )
 the carrier of S c= the carrier of T by YELLOW_0:def_13;
then reconsider C = A as Subset of T by XBOOLE_1:1;
set F = finsups C;
assume A3: ex_sup_of A,T ; ::_thesis: "\/" (A,T) in the carrier of S
then A4: sup (finsups C) = sup C by WAYBEL_0:55;
 finsups C c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups C or x in the carrier of S )
assume  x in finsups C ; ::_thesis: x in the carrier of S
then consider Y being finite Subset of C such that
A5: x = "\/" (Y,T) and
 ex_sup_of Y,T ;
reconsider Y = Y as finite Subset of T by XBOOLE_1:1;
reconsider Z = Y as finite Subset of S by XBOOLE_1:1;
assume A6: not x in the carrier of S ; ::_thesis: contradiction
then  Z <> {} by A1, A5;
hence  contradiction by A5, A6, Th15; ::_thesis: verum
end;
then reconsider G = finsups C as non empty Subset of S ;
reconsider G = G as non empty directed Subset of S by WAYBEL10:23;
A7: now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_
ex_sup_of_Y,T
let Y be finite Subset of C; ::_thesis: ( Y <> {} implies ex_sup_of Y,T )
 Y c= the carrier of T by XBOOLE_1:1;
hence  ( Y <> {} implies ex_sup_of Y,T ) by YELLOW_0:54; ::_thesis: verum
end;
A8: now__::_thesis:_for_x_being_Element_of_T_st_x_in_finsups_C_holds_
ex_Y_being_finite_Subset_of_C_st_
(_ex_sup_of_Y,T_&_x_=_"\/"_(Y,T)_)
let x be Element of T; ::_thesis: ( x in finsups C implies ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) ) )
assume  x in finsups C ; ::_thesis: ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) )
then  ex Y being finite Subset of C st
( x = "\/" (Y,T) & ex_sup_of Y,T ) ;
hence  ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) ) ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_
"\/"_(Y,T)_in_finsups_C
let Y be finite Subset of C; ::_thesis: ( Y <> {} implies "\/" (Y,T) in finsups C )
reconsider Z = Y as finite Subset of T by XBOOLE_1:1;
assume  Y <> {} ; ::_thesis: "\/" (Y,T) in finsups C
then  ex_sup_of Z,T by YELLOW_0:54;
hence  "\/" (Y,T) in finsups C ; ::_thesis: verum
end;
then  ex_sup_of G,T by A3, A7, A8, WAYBEL_0:53;
hence  "\/" (A,T) in the carrier of S by A2, A4, WAYBEL_0:def_4; ::_thesis: verum
end;

theorem Th18: :: WAYBEL21:18
for T being complete LATTICE
for S being non empty full SubRelStr of T st S is infs-inheriting holds
S is complete
proof
let T be complete LATTICE; ::_thesis: for S being non empty full SubRelStr of T st S is infs-inheriting holds
S is complete
let S be non empty full SubRelStr of T; ::_thesis: ( S is infs-inheriting implies S is complete )
assume A1: S is infs-inheriting ; ::_thesis: S is complete
now__::_thesis:_for_X_being_set_holds_ex_inf_of_X,S
let X be set ; ::_thesis: ex_inf_of X,S
set Y = X /\ the carrier of S;
reconsider Y = X /\ the carrier of S as Subset of S by XBOOLE_1:17;
A2: ex_inf_of Y,T by YELLOW_0:17;
then  "/\" (Y,T) in the carrier of S by A1, YELLOW_0:def_18;
then  ex_inf_of Y,S by A2, YELLOW_0:63;
hence  ex_inf_of X,S by YELLOW_0:50; ::_thesis: verum
end;
hence  S is complete by YELLOW_2:25; ::_thesis: verum
end;

theorem :: WAYBEL21:19
for T being complete LATTICE
for S being non empty full SubRelStr of T st S is sups-inheriting holds
S is complete
proof
let T be complete LATTICE; ::_thesis: for S being non empty full SubRelStr of T st S is sups-inheriting holds
S is complete
let S be non empty full SubRelStr of T; ::_thesis: ( S is sups-inheriting implies S is complete )
assume A1: S is sups-inheriting ; ::_thesis: S is complete
now__::_thesis:_for_X_being_set_holds_ex_sup_of_X,S
let X be set ; ::_thesis: ex_sup_of X,S
set Y = X /\ the carrier of S;
reconsider Y = X /\ the carrier of S as Subset of S by XBOOLE_1:17;
A2: ex_sup_of Y,T by YELLOW_0:17;
then  "\/" (Y,T) in the carrier of S by A1, YELLOW_0:def_19;
then  ex_sup_of Y,S by A2, YELLOW_0:64;
hence  ex_sup_of X,S by YELLOW_0:50; ::_thesis: verum
end;
hence  S is complete by YELLOW_2:24; ::_thesis: verum
end;

theorem :: WAYBEL21:20
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting
proof
let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting
let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting
let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting implies S2 is infs-inheriting )
assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is infs-inheriting or S2 is infs-inheriting )
assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is infs-inheriting or S2 is infs-inheriting )
assume A3: for X being Subset of S1 st ex_inf_of X,T1 holds
"/\" (X,T1) in the carrier of S1 ; :: according to YELLOW_0:def_18 ::_thesis: S2 is infs-inheriting
let X be Subset of S2; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 )
reconsider Y = X as Subset of S1 by A2;
assume A4: ex_inf_of X,T2 ; ::_thesis: "/\" (X,T2) in the carrier of S2
then  "/\" (Y,T1) in the carrier of S1 by A1, A3, YELLOW_0:14;
hence  "/\" (X,T2) in the carrier of S2 by A1, A2, A4, YELLOW_0:27; ::_thesis: verum
end;

theorem :: WAYBEL21:21
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds
S2 is sups-inheriting
proof
let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds
S2 is sups-inheriting
let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds
S2 is sups-inheriting
let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting implies S2 is sups-inheriting )
assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is sups-inheriting or S2 is sups-inheriting )
assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is sups-inheriting or S2 is sups-inheriting )
assume A3: for X being Subset of S1 st ex_sup_of X,T1 holds
"\/" (X,T1) in the carrier of S1 ; :: according to YELLOW_0:def_19 ::_thesis: S2 is sups-inheriting
let X be Subset of S2; :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 )
reconsider Y = X as Subset of S1 by A2;
assume A4: ex_sup_of X,T2 ; ::_thesis: "\/" (X,T2) in the carrier of S2
then  "\/" (Y,T1) in the carrier of S1 by A1, A3, YELLOW_0:14;
hence  "\/" (X,T2) in the carrier of S2 by A1, A2, A4, YELLOW_0:26; ::_thesis: verum
end;

theorem :: WAYBEL21:22
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting
proof
let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting
let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting
let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting )
assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is directed-sups-inheriting or S2 is directed-sups-inheriting )
 RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ;
then reconsider R = S2 as full SubRelStr of T1 by A1, Th12;
assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is directed-sups-inheriting or S2 is directed-sups-inheriting )
then A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_0:57;
assume A4: for X being directed Subset of S1 st X <> {} & ex_sup_of X,T1 holds
"\/" (X,T1) in the carrier of S1 ; :: according to WAYBEL_0:def_4 ::_thesis: S2 is directed-sups-inheriting
let X be directed Subset of S2; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 )
assume A5: X <> {} ; ::_thesis: ( not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 )
reconsider Y = X as directed Subset of S1 by A3, WAYBEL_0:3;
assume A6: ex_sup_of X,T2 ; ::_thesis: "\/" (X,T2) in the carrier of S2
then  "\/" (Y,T1) in the carrier of S1 by A1, A4, A5, YELLOW_0:14;
hence  "\/" (X,T2) in the carrier of S2 by A1, A2, A6, YELLOW_0:26; ::_thesis: verum
end;

theorem :: WAYBEL21:23
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting
proof
let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting
let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting
let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting )
assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is filtered-infs-inheriting or S2 is filtered-infs-inheriting )
 RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ;
then reconsider R = S2 as full SubRelStr of T1 by A1, Th12;
assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is filtered-infs-inheriting or S2 is filtered-infs-inheriting )
then A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_0:57;
assume A4: for X being filtered Subset of S1 st X <> {} & ex_inf_of X,T1 holds
"/\" (X,T1) in the carrier of S1 ; :: according to WAYBEL_0:def_3 ::_thesis: S2 is filtered-infs-inheriting
let X be filtered Subset of S2; :: according to WAYBEL_0:def_3 ::_thesis: ( X = {} or not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 )
assume A5: X <> {} ; ::_thesis: ( not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 )
reconsider Y = X as filtered Subset of S1 by A3, WAYBEL_0:4;
assume A6: ex_inf_of X,T2 ; ::_thesis: "/\" (X,T2) in the carrier of S2
then  "/\" (Y,T1) in the carrier of S1 by A1, A4, A5, YELLOW_0:14;
hence  "/\" (X,T2) in the carrier of S2 by A1, A2, A6, YELLOW_0:27; ::_thesis: verum
end;

begin

theorem Th24: :: WAYBEL21:24
for S, T being non empty TopSpace
for N being net of S
for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)
proof
let S, T be non empty TopSpace; ::_thesis: for N being net of S
for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)
let N be net of S; ::_thesis: for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)
A1: [#] T <> {} ;
let f be Function of S,T; ::_thesis: ( f is continuous implies f .: (Lim N) c= Lim (f * N) )
assume A2: f is continuous ; ::_thesis: f .: (Lim N) c= Lim (f * N)
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f .: (Lim N) or p in Lim (f * N) )
assume A3: p in f .: (Lim N) ; ::_thesis: p in Lim (f * N)
then reconsider p = p as Point of T ;
consider x being set  such that
A4: x in the carrier of S and
A5: x in Lim N and
A6: p = f . x by A3, FUNCT_2:64;
reconsider x = x as Element of S by A4;
now__::_thesis:_for_V_being_a_neighborhood_of_p_holds_f_*_N_is_eventually_in_V
let V be a_neighborhood of p; ::_thesis: f * N is_eventually_in V
A7: p in Int V by CONNSP_2:def_1;
A8: x in f " (Int V) by A6, A7, FUNCT_2:38;
 f " (Int V) is open by A1, A2, TOPS_2:43;
then  f " (Int V) is a_neighborhood of x by A8, CONNSP_2:3;
then  N is_eventually_in f " (Int V) by A5, YELLOW_6:def_15;
then consider i being Element of N such that
A9: for j being Element of N st j >= i holds
N . j in f " (Int V) by WAYBEL_0:def_11;
A10: the mapping of (f * N) = f * the mapping of N by WAYBEL_9:def_8;
A11: 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 i9 = i as Element of (f * N) ;
thus  f * N is_eventually_in V ::_thesis: verum
proof
take  i9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (f * N) holds
( not i9 <= b1 or (f * N) . b1 in V )
let j9 be Element of (f * N); ::_thesis: ( not i9 <= j9 or (f * N) . j9 in V )
reconsider j = j9 as Element of N by A11;
A12: f . (N . j) = (f * N) . j9 by A10, FUNCT_2:15;
assume  j9 >= i9 ; ::_thesis: (f * N) . j9 in V
then  N . j in f " (Int V) by A9, A11, YELLOW_0:1;
then A13: f . (N . j) in Int V by FUNCT_2:38;
 Int V c= V by TOPS_1:16;
hence  (f * N) . j9 in V by A12, A13; ::_thesis: verum
end;
end;
hence  p in Lim (f * N) by YELLOW_6:def_15; ::_thesis: verum
end;

definition
let T be non empty RelStr ;
let N be non empty NetStr over T;
redefine attr N is antitone  means :Def2: :: WAYBEL21:def 2
 for i, j being Element of N st i <= j holds
N . i >= N . j;
compatibility
 ( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j )
proof
hereby  ::_thesis: ( ( for i, j being Element of N st i <= j holds
N . i >= N . j ) implies N is antitone )
assume  N is antitone ; ::_thesis: for i, j being Element of N st i <= j holds
N . i >= N . j
then A1: netmap (N,T) is antitone by WAYBEL_0:def_10;
let i, j be Element of N; ::_thesis: ( i <= j implies N . i >= N . j )
assume  i <= j ; ::_thesis: N . i >= N . j
hence  N . i >= N . j by A1, WAYBEL_0:def_5; ::_thesis: verum
end;
assume A2: for i, j being Element of N st i <= j holds
N . i >= N . j ; ::_thesis: N is antitone
let i, j be Element of N; :: according to WAYBEL_0:def_5,WAYBEL_0:def_10 ::_thesis: ( not i <= j or for b1, b2 being Element of the carrier of T holds
( not b1 = (netmap (N,T)) . i or not b2 = (netmap (N,T)) . j or b2 <= b1 ) )
A3: N . i = (netmap (N,T)) . i ;
 N . j = (netmap (N,T)) . j ;
hence  ( not i <= j or for b1, b2 being Element of the carrier of T holds
( not b1 = (netmap (N,T)) . i or not b2 = (netmap (N,T)) . j or b2 <= b1 ) ) by A2, A3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines antitone WAYBEL21:def_2_:_
 for T being non empty RelStr
for N being non empty NetStr over T holds
( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j );

registration
let T be non empty reflexive RelStr ;
let x be Element of T;
cluster{x} opp+id  ->  transitive directed monotone antitone ;
coherence
 ( {x} opp+id is transitive & {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone )
proof
set N = {x} opp+id ;
A1: the carrier of ({x} opp+id) = {x} by YELLOW_9:7;
thus  {x} opp+id is transitive ::_thesis: ( {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone )
proof
let i, j, k be Element of ({x} opp+id); :: according to YELLOW_0:def_2 ::_thesis: ( not i <= j or not j <= k or i <= k )
 i = x by A1, TARSKI:def_1;
hence  ( not i <= j or not j <= k or i <= k ) by A1, TARSKI:def_1; ::_thesis: verum
end;
thus  {x} opp+id is directed ::_thesis: ( {x} opp+id is monotone & {x} opp+id is antitone )
proof
let i, j be Element of ({x} opp+id); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of ({x} opp+id) st
( i <= b1 & j <= b1 )
A2: i = x by A1, TARSKI:def_1;
A3: i <= i ;
 j <= i by A1, A2, TARSKI:def_1;
hence  ex b1 being Element of the carrier of ({x} opp+id) st
( i <= b1 & j <= b1 ) by A3; ::_thesis: verum
end;
thus  {x} opp+id is monotone ::_thesis: {x} opp+id is antitone
proof
let i, j be Element of ({x} opp+id); :: according to WAYBEL_0:def_9,WAYBEL_1:def_2 ::_thesis: ( not i <= j or (netmap (({x} opp+id),T)) . i <= (netmap (({x} opp+id),T)) . j )
A4: i = x by A1, TARSKI:def_1;
 j = x by A1, TARSKI:def_1;
hence  ( not i <= j or (netmap (({x} opp+id),T)) . i <= (netmap (({x} opp+id),T)) . j ) by A4, YELLOW_0:def_1; ::_thesis: verum
end;
let i, j be Element of ({x} opp+id); :: according to WAYBEL21:def_2 ::_thesis: ( i <= j implies ({x} opp+id) . i >= ({x} opp+id) . j )
A5: i = x by A1, TARSKI:def_1;
 j = x by A1, TARSKI:def_1;
hence  ( i <= j implies ({x} opp+id) . i >= ({x} opp+id) . j ) by A5, YELLOW_0:def_1; ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
cluster non empty reflexive transitive strict directed monotone antitone for NetStr over T;
existence
 ex b1 being net of T st
( b1 is monotone & b1 is antitone & b1 is reflexive & b1 is strict )
proof
set x = the Element of T;
take  { the Element of T} opp+id ; ::_thesis: ( { the Element of T} opp+id is monotone & { the Element of T} opp+id is antitone & { the Element of T} opp+id is reflexive & { the Element of T} opp+id is strict )
thus  ( { the Element of T} opp+id is monotone & { the Element of T} opp+id is antitone & { the Element of T} opp+id is reflexive & { the Element of T} opp+id is strict ) ; ::_thesis: verum
end;
end;

registration
let T be non empty RelStr ;
let F be non empty Subset of T;
clusterF opp+id  ->  antitone ;
coherence
 F opp+id is antitone
proof
let i, j be Element of (F opp+id); :: according to WAYBEL21:def_2 ::_thesis: ( i <= j implies (F opp+id) . i >= (F opp+id) . j )
A1: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
then reconsider x = i, y = j as Element of (T opp) by YELLOW_0:58;
assume  i <= j ; ::_thesis: (F opp+id) . i >= (F opp+id) . j
then  x <= y by A1, YELLOW_0:59;
then  ~ x >= ~ y by YELLOW_7:1;
then  (F opp+id) . i >= ~ y by YELLOW_9:7;
hence  (F opp+id) . i >= (F opp+id) . j by YELLOW_9:7; ::_thesis: verum
end;
end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let N be non empty antitone NetStr over S;
clusterf * N ->  antitone ;
coherence
 f * N is antitone
proof
let i, j be Element of (f * N); :: according to WAYBEL21:def_2 ::_thesis: ( i <= j implies (f * N) . i >= (f * N) . j )
A1: the mapping of (f * N) = f * the mapping of N by WAYBEL_9:def_8;
A2: 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 x = i, y = j as Element of N ;
assume  i <= j ; ::_thesis: (f * N) . i >= (f * N) . j
then  x <= y by A2, YELLOW_0:1;
then  N . x >= N . y by Def2;
then  f . (N . x) >= f . (N . y) by WAYBEL_1:def_2;
then  (f * N) . i >= f . (N . y) by A1, FUNCT_2:15;
hence  (f * N) . i >= (f * N) . j by A1, FUNCT_2:15; ::_thesis: verum
end;
end;

theorem Th25: :: WAYBEL21:25
for S being complete LATTICE
for N being net of S holds  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
proof
let S be complete LATTICE; ::_thesis: for N being net of S holds  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
let N be net of S; ::_thesis:  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
set X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  ;
  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  or x in the carrier of S )
assume  x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  ; ::_thesis: x in the carrier of S
then  ex j being Element of N st x = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) ;
hence  x in the carrier of S ; ::_thesis: verum
end;
then reconsider X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  as Subset of S ;
 ( not X is empty & X is directed ) by WAYBEL11:30;
hence   {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S ; ::_thesis: verum
end;

theorem :: WAYBEL21:26
for S being non empty Poset
for N being reflexive monotone net of S holds  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
proof
let S be non empty Poset; ::_thesis: for N being reflexive monotone net of S holds  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
let N be reflexive monotone net of S; ::_thesis:  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
set X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  ;
set jj = the Element of N;
A1: "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,S) in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  ;
  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  or x in the carrier of S )
assume  x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  ; ::_thesis: x in the carrier of S
then  ex j being Element of N st x = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) ;
hence  x in the carrier of S ; ::_thesis: verum
end;
then reconsider X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  as non empty Subset of S by A1;
 X is directed
proof
let x, y be Element of S; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 ) )
assume  x in X ; ::_thesis: ( not y in X or ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 ) )
then consider j1 being Element of N such that
A2: x = "/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,S) ;
assume  y in X ; ::_thesis: ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 )
then consider j2 being Element of N such that
A3: y = "/\" ( {  (N . i) where i is Element of N : i >= j2  }  ,S) ;
reconsider j1 = j1, j2 = j2 as Element of N ;
 [#] N is directed by WAYBEL_0:def_6;
then consider j being Element of N such that
 j in [#] N and
A4: j >= j1 and
A5: j >= j2 by WAYBEL_0:def_1;
set z = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S);
take  "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) ; ::_thesis: ( "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) in X & x <= "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) & y <= "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) )
thus  "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) in X ; ::_thesis: ( x <= "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) & y <= "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) )
deffunc H1( Element of N) ->  set =  {  (N . i) where i is Element of N : i >= $1  }  ;
A6: for j being Element of N holds ex_inf_of H1(j),S
proof
let j be Element of N; ::_thesis: ex_inf_of H1(j),S
reconsider j9 = j as Element of N ;
now__::_thesis:_ex_x_being_Element_of_the_carrier_of_S_st_
(_x_is_<=_than_H1(j)_&_(_for_y_being_Element_of_S_st_y_is_<=_than_H1(j)_holds_
y_<=_x_)_)
take x = N . j; ::_thesis: ( x is_<=_than H1(j) & ( for y being Element of S st y is_<=_than H1(j) holds
y <= x ) )
 j9 <= j9 ;
then A7: x in H1(j) ;
thus  x is_<=_than H1(j) ::_thesis: for y being Element of S st y is_<=_than H1(j) holds
y <= x
proof
let y be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not y in H1(j) or x <= y )
assume  y in H1(j) ; ::_thesis: x <= y
then  ex i being Element of N st
( y = N . i & i >= j ) ;
hence  x <= y by WAYBEL11:def_9; ::_thesis: verum
end;
let y be Element of S; ::_thesis: ( y is_<=_than H1(j) implies y <= x )
assume  y is_<=_than H1(j) ; ::_thesis: y <= x
hence  y <= x by A7, LATTICE3:def_8; ::_thesis: verum
end;
hence  ex_inf_of H1(j),S by YELLOW_0:16; ::_thesis: verum
end;
then A8: ex_inf_of H1(j1),S ;
A9: ex_inf_of H1(j2),S by A6;
A10: ex_inf_of H1(j),S by A6;
set A =  {  (N . i) where i is Element of N : i >= j  }  ;
  {  (N . i) where i is Element of N : i >= j  }  c=  {  (N . k) where k is Element of N : k >= j1  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (N . i) where i is Element of N : i >= j  }  or a in  {  (N . k) where k is Element of N : k >= j1  }  )
assume  a in  {  (N . i) where i is Element of N : i >= j  }  ; ::_thesis: a in  {  (N . k) where k is Element of N : k >= j1  }
then consider k being Element of N such that
A11: a = N . k and
A12: k >= j ;
reconsider k = k as Element of N ;
 k >= j1 by A4, A12, ORDERS_2:3;
hence  a in  {  (N . k) where k is Element of N : k >= j1  }  by A11; ::_thesis: verum
end;
hence  "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) >= x by A2, A8, A10, YELLOW_0:35; ::_thesis: y <= "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)
  {  (N . i) where i is Element of N : i >= j  }  c=  {  (N . k) where k is Element of N : k >= j2  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (N . i) where i is Element of N : i >= j  }  or a in  {  (N . k) where k is Element of N : k >= j2  }  )
assume  a in  {  (N . i) where i is Element of N : i >= j  }  ; ::_thesis: a in  {  (N . k) where k is Element of N : k >= j2  }
then consider k being Element of N such that
A13: a = N . k and
A14: k >= j ;
reconsider k = k as Element of N ;
 k >= j2 by A5, A14, ORDERS_2:3;
hence  a in  {  (N . k) where k is Element of N : k >= j2  }  by A13; ::_thesis: verum
end;
hence  y <= "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S) by A3, A9, A10, YELLOW_0:35; ::_thesis: verum
end;
hence   {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S ; ::_thesis: verum
end;

theorem Th27: :: WAYBEL21:27
for S being non empty 1-sorted
for N being non empty NetStr over S
for X being set st rng the mapping of N c= X holds
N is_eventually_in X
proof
let S be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over S
for X being set st rng the mapping of N c= X holds
N is_eventually_in X
let N be non empty NetStr over S; ::_thesis: for X being set st rng the mapping of N c= X holds
N is_eventually_in X
let X be set ; ::_thesis: ( rng the mapping of N c= X implies N is_eventually_in X )
assume A1: rng the mapping of N c= X ; ::_thesis: N is_eventually_in X
set i = the Element of N;
take  the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in X )
let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in X )
 N . j in rng the mapping of N by FUNCT_2:4;
hence  ( not the Element of N <= j or N . j in X ) by A1; ::_thesis: verum
end;

theorem Th28: :: WAYBEL21:28
for R being non empty /\-complete Poset
for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F
proof
let R be non empty /\-complete Poset; ::_thesis: for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F
let F be non empty filtered Subset of R; ::_thesis: lim_inf (F opp+id) = inf F
set N = F opp+id ;
defpred S1[ set ] means verum;
deffunc H1( Element of (F opp+id)) ->  Element of the carrier of R = inf F;
deffunc H2( Element of (F opp+id)) ->  Element of the carrier of R = "/\" ( {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= $1  }  ,R);
A1: for v being Element of (F opp+id) st S1[v] holds
H1(v) = H2(v)
proof
let v be Element of (F opp+id); ::_thesis: ( S1[v] implies H1(v) = H2(v) )
set X =  {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= v  }  ;
A2: the carrier of (F opp+id) = F by YELLOW_9:7;
then  v in F ;
then reconsider j = v as Element of R ;
reconsider vv = v as Element of (F opp+id) ;
A3:  {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= v  }  c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= v  }  or x in F )
assume  x in  {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= v  }  ; ::_thesis: x in F
then consider i being Element of (F opp+id) such that
A4: x = (F opp+id) . i and
 i >= v ;
reconsider i = i as Element of (F opp+id) ;
 x = i by A4, YELLOW_9:7;
hence  x in F by A2; ::_thesis: verum
end;
 vv <= vv ;
then  (F opp+id) . v in  {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= v  }  ;
then reconsider X =  {  ((F opp+id) . i) where i is Element of (F opp+id) : i >= v  }  as non empty Subset of R by A3, XBOOLE_1:1;
A5: ex_inf_of F,R by WAYBEL_0:76;
A6: ex_inf_of X,R by WAYBEL_0:76;
then A7: inf X >= inf F by A3, A5, YELLOW_0:35;
 F is_>=_than inf X
proof
let a be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not a in F or inf X <= a )
assume  a in F ; ::_thesis: inf X <= a
then consider b being Element of R such that
A8: b in F and
A9: a >= b and
A10: j >= b by A2, WAYBEL_0:def_2;
reconsider k = b as Element of (F opp+id) by A8, YELLOW_9:7;
A11: F opp+id is full SubRelStr of R opp by YELLOW_9:7;
A12: j ~ <= b ~ by A10, LATTICE3:9;
A13: (F opp+id) . k = b by YELLOW_9:7;
 k >= vv by A11, A12, YELLOW_0:60;
then  b in X by A13;
then A14: {b} c= X by ZFMISC_1:31;
A15: ex_inf_of {b},R by YELLOW_0:38;
 inf {b} = b by YELLOW_0:39;
then  b >= inf X by A6, A14, A15, YELLOW_0:35;
hence  inf X <= a by A9, YELLOW_0:def_2; ::_thesis: verum
end;
then  inf F >= "/\" (X,R) by A5, YELLOW_0:31;
hence  ( S1[v] implies H1(v) = H2(v) ) by A7, ORDERS_2:2; ::_thesis: verum
end;
A16:  {  H1(j) where j is Element of (F opp+id) : S1[j]  }  =  {  H2(k) where k is Element of (F opp+id) : S1[k]  }  from FRAENKEL:sch_6(A1);
A17: ex j being Element of (F opp+id) st S1[j] ;
  {  (inf F) where j is Element of (F opp+id) : S1[j]  }  = {(inf F)} from LATTICE3:sch_1(A17);
hence  lim_inf (F opp+id) = "\/" ({(inf F)},R) by A16, WAYBEL11:def_6
.= inf F by YELLOW_0:39 ;
::_thesis: verum
end;

theorem Th29: :: WAYBEL21:29
for S, T being non empty /\-complete Poset
for X being non empty filtered Subset of S
for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)
proof
let S, T be non empty /\-complete Poset; ::_thesis: for X being non empty filtered Subset of S
for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)
let X be non empty filtered Subset of S; ::_thesis: for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)
let f be monotone Function of S,T; ::_thesis: lim_inf (f * (X opp+id)) = inf (f .: X)
set M = X opp+id ;
set N = f * (X opp+id);
deffunc H1( Element of (f * (X opp+id))) ->  set =  {  ((f * (X opp+id)) . i) where i is Element of (f * (X opp+id)) : i >= $1  }  ;
deffunc H2( Element of (f * (X opp+id))) ->  Element of the carrier of T = "/\" (H1($1),T);
A1: RelStr(# the carrier of (f * (X opp+id)), the InternalRel of (f * (X opp+id)) #) = RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) by WAYBEL_9:def_8;
A2: the mapping of (f * (X opp+id)) = f * the mapping of (X opp+id) by WAYBEL_9:def_8;
A3: the carrier of (X opp+id) = X by YELLOW_9:7;
A4: the mapping of (X opp+id) = id X by WAYBEL19:27;
defpred S1[ set ] means verum;
deffunc H3( set ) ->  Element of the carrier of T = inf (f .: X);
A5: for j being Element of (f * (X opp+id)) st S1[j] holds
H2(j) = H3(j)
proof
let j be Element of (f * (X opp+id)); ::_thesis: ( S1[j] implies H2(j) = H3(j) )
reconsider j = j as Element of (f * (X opp+id)) ;
A6: [#] (f * (X opp+id)) is directed by WAYBEL_0:def_6;
then consider i9 being Element of (f * (X opp+id)) such that
 i9 in [#] (f * (X opp+id)) and
A7: i9 >= j and
 i9 >= j by WAYBEL_0:def_1;
A8: H1(j) c= f .: X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in H1(j) or a in f .: X )
assume  a in H1(j) ; ::_thesis: a in f .: X
then consider i being Element of (f * (X opp+id)) such that
A9: a = (f * (X opp+id)) . i and
 i >= j ;
reconsider i = i as Element of (f * (X opp+id)) ;
reconsider i9 = i as Element of (X opp+id) by A1;
A10: (f * (X opp+id)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15
.= f . i9 by A3, FUNCT_1:18 ;
 i9 in X by A3;
hence  a in f .: X by A9, A10, FUNCT_2:35; ::_thesis: verum
end;
then A11: H1(j) c= the carrier of T by XBOOLE_1:1;
 (f * (X opp+id)) . i9 in H1(j) by A7;
then A12: ex_inf_of H1(j),T by A11, WAYBEL_0:76;
A13: ex_inf_of f .: X,T by WAYBEL_0:76;
then A14: H2(j) >= inf (f .: X) by A8, A12, YELLOW_0:35;
 H2(j) is_<=_than f .: X
proof
let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or H2(j) <= x )
assume  x in f .: X ; ::_thesis: H2(j) <= x
then consider y being set  such that
A15: y in the carrier of S and
A16: y in X and
A17: x = f . y by FUNCT_2:64;
reconsider y = y as Element of (f * (X opp+id)) by A1, A16, YELLOW_9:7;
consider i being Element of (f * (X opp+id)) such that
 i in [#] (f * (X opp+id)) and
A18: i >= y and
A19: i >= j by A6, WAYBEL_0:def_1;
 i in X by A1, A3;
then reconsider xi = i, xy = y as Element of S by A15;
 X opp+id is full SubRelStr of S opp by YELLOW_9:7;
then  f * (X opp+id) is full SubRelStr of S opp by A1, Th12;
then  xi ~ >= xy ~ by A18, YELLOW_0:59;
then  xi <= xy by LATTICE3:9;
then A20: f . xi <= x by A17, WAYBEL_1:def_2;
(f * (X opp+id)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15
.= f . xi by A1, A3, FUNCT_1:18 ;
then  f . xi in H1(j) by A19;
then  f . xi >= H2(j) by A12, YELLOW_4:2;
hence  H2(j) <= x by A20, ORDERS_2:3; ::_thesis: verum
end;
then  H2(j) <= inf (f .: X) by A13, YELLOW_0:31;
hence  ( S1[j] implies H2(j) = H3(j) ) by A14, ORDERS_2:2; ::_thesis: verum
end;
A21: ex j being Element of (f * (X opp+id)) st S1[j] ;
 {  H2(j) where j is Element of (f * (X opp+id)) : S1[j]  }  =  {  H3(j) where j is Element of (f * (X opp+id)) : S1[j]  }  from FRAENKEL:sch_6(A5)
.=  {  (inf (f .: X)) where j is Element of (f * (X opp+id)) : S1[j]  }
.= {(inf (f .: X))} from LATTICE3:sch_1(A21) ;
hence  lim_inf (f * (X opp+id)) = sup {(inf (f .: X))} by WAYBEL11:def_6
.= inf (f .: X) by YELLOW_0:39 ;
::_thesis: verum
end;

theorem Th30: :: WAYBEL21:30
for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
proof
let S, T be non empty TopPoset; ::_thesis: for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
let X be non empty filtered Subset of S; ::_thesis: for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
let f be monotone Function of S,T; ::_thesis: for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
let Y be non empty filtered Subset of T; ::_thesis: ( Y = f .: X implies f * (X opp+id) is subnet of Y opp+id )
assume A1: Y = f .: X ; ::_thesis: f * (X opp+id) is subnet of Y opp+id
set N = f * (X opp+id);
set M = Y opp+id ;
A2: RelStr(# the carrier of (f * (X opp+id)), the InternalRel of (f * (X opp+id)) #) = RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) by WAYBEL_9:def_8;
A3: the mapping of (f * (X opp+id)) = f * the mapping of (X opp+id) by WAYBEL_9:def_8;
A4: the carrier of (Y opp+id) = Y by YELLOW_9:7;
A5: the mapping of (Y opp+id) = id Y by WAYBEL19:27;
A6: the carrier of (X opp+id) = X by YELLOW_9:7;
 the mapping of (X opp+id) = id X by WAYBEL19:27;
then A7: the mapping of (f * (X opp+id)) = f | X by A3, RELAT_1:65;
then A8: rng the mapping of (f * (X opp+id)) = f .: X by RELAT_1:115;
 dom the mapping of (f * (X opp+id)) = X by A2, A6, FUNCT_2:def_1;
then reconsider g = f | X as Function of (f * (X opp+id)),(Y opp+id) by A1, A2, A4, A6, A7, A8, FUNCT_2:def_1, RELSET_1:4;
take  g ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g & ( for b1 being Element of the carrier of (Y opp+id) ex b2 being Element of the carrier of (f * (X opp+id)) st
for b3 being Element of the carrier of (f * (X opp+id)) holds
( not b2 <= b3 or b1 <= g . b3 ) ) )
thus  the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g by A1, A5, A7, A8, RELAT_1:53; ::_thesis: for b1 being Element of the carrier of (Y opp+id) ex b2 being Element of the carrier of (f * (X opp+id)) st
for b3 being Element of the carrier of (f * (X opp+id)) holds
( not b2 <= b3 or b1 <= g . b3 )
let m be Element of (Y opp+id); ::_thesis: ex b1 being Element of the carrier of (f * (X opp+id)) st
for b2 being Element of the carrier of (f * (X opp+id)) holds
( not b1 <= b2 or m <= g . b2 )
consider n being set  such that
A9: n in the carrier of S and
A10: n in X and
A11: m = f . n by A1, A4, FUNCT_2:64;
reconsider n = n as Element of (f * (X opp+id)) by A2, A10, YELLOW_9:7;
take  n ; ::_thesis: for b1 being Element of the carrier of (f * (X opp+id)) holds
( not n <= b1 or m <= g . b1 )
let p be Element of (f * (X opp+id)); ::_thesis: ( not n <= p or m <= g . p )
 p in X by A2, A6;
then reconsider n9 = n, p9 = p as Element of S by A9;
reconsider fp = f . p9 as Element of (Y opp+id) by A1, A2, A4, A6, FUNCT_2:35;
 X opp+id is SubRelStr of S opp by YELLOW_9:7;
then A12: f * (X opp+id) is SubRelStr of S opp by A2, Th12;
A13: Y opp+id is full SubRelStr of T opp by YELLOW_9:7;
assume  n <= p ; ::_thesis: m <= g . p
then  n9 ~ <= p9 ~ by A12, YELLOW_0:59;
then  n9 >= p9 by LATTICE3:9;
then  f . n9 >= f . p9 by WAYBEL_1:def_2;
then  (f . n9) ~ <= (f . p9) ~ by LATTICE3:9;
then  fp >= m by A11, A13, YELLOW_0:60;
hence  m <= g . p by A2, A6, FUNCT_1:49; ::_thesis: verum
end;

theorem :: WAYBEL21:31
for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))
proof
let S, T be non empty TopPoset; ::_thesis: for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))
let X be non empty filtered Subset of S; ::_thesis: for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))
let f be monotone Function of S,T; ::_thesis: for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))
let Y be non empty filtered Subset of T; ::_thesis: ( Y = f .: X implies Lim (Y opp+id) c= Lim (f * (X opp+id)) )
assume  Y = f .: X ; ::_thesis: Lim (Y opp+id) c= Lim (f * (X opp+id))
then  f * (X opp+id) is subnet of Y opp+id by Th30;
hence  Lim (Y opp+id) c= Lim (f * (X opp+id)) by YELLOW_6:32; ::_thesis: verum
end;

theorem Th32: :: WAYBEL21:32
for S being non empty reflexive RelStr
for D being non empty Subset of S holds
( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )
proof
let S be non empty reflexive RelStr ; ::_thesis: for D being non empty Subset of S holds
( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )
let D be non empty Subset of S; ::_thesis: ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )
set N = Net-Str D;
A1: dom (id D) = D ;
 rng (id D) = D ;
then reconsider g = id D as Function of D, the carrier of S by A1, FUNCT_2:def_1, RELSET_1:4;
 (id the carrier of S) | D = id D by FUNCT_3:1;
then A2: Net-Str D = NetStr(# D,( the InternalRel of S |_2 D),g #) by WAYBEL17:def_4;
then  the InternalRel of (Net-Str D) c= the InternalRel of S by XBOOLE_1:17;
hence  ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S ) by A2, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;

theorem Th33: :: WAYBEL21:33
for S, T being non empty up-complete Poset
for f being monotone Function of S,T
for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)
proof
let S, T be non empty up-complete Poset; ::_thesis: for f being monotone Function of S,T
for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)
let f be monotone Function of S,T; ::_thesis: for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)
let X be non empty directed Subset of S; ::_thesis: lim_inf (f * (Net-Str X)) = sup (f .: X)
set M = Net-Str X;
set N = f * (Net-Str X);
deffunc H1( Element of (f * (Net-Str X))) ->  set =  {  ((f * (Net-Str X)) . i) where i is Element of (f * (Net-Str X)) : i >= $1  }  ;
deffunc H2( Element of (f * (Net-Str X))) ->  Element of the carrier of T = "/\" (H1($1),T);
set NT =  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  ;
A1: RelStr(# the carrier of (f * (Net-Str X)), the InternalRel of (f * (Net-Str X)) #) = RelStr(# the carrier of (Net-Str X), the InternalRel of (Net-Str X) #) by WAYBEL_9:def_8;
A2: the mapping of (f * (Net-Str X)) = f * the mapping of (Net-Str X) by WAYBEL_9:def_8;
A3: the carrier of (Net-Str X) = X by Th32;
A4: the mapping of (Net-Str X) = id X by Th32;
A5: now__::_thesis:_for_i_being_Element_of_(f_*_(Net-Str_X))_holds_(f_*_(Net-Str_X))_._i_=_f_._i
let i be Element of (f * (Net-Str X)); ::_thesis: (f * (Net-Str X)) . i = f . i
thus (f * (Net-Str X)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15
.= f . i by A1, A3, FUNCT_1:18 ; ::_thesis: verum
end;
A6: for i being Element of (f * (Net-Str X)) holds H2(i) = f . i
proof
let i be Element of (f * (Net-Str X)); ::_thesis: H2(i) = f . i
 i in X by A1, A3;
then reconsider x = i as Element of S ;
A7: i <= i ;
 (f * (Net-Str X)) . i = f . x by A5;
then  f . x in H1(i) by A7;
then A8: for z being Element of T st z is_<=_than H1(i) holds
z <= f . x by LATTICE3:def_8;
 f . x is_<=_than H1(i)
proof
let z be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not z in H1(i) or f . x <= z )
assume  z in H1(i) ; ::_thesis: f . x <= z
then consider j being Element of (f * (Net-Str X)) such that
A9: z = (f * (Net-Str X)) . j and
A10: j >= i ;
reconsider j = j as Element of (f * (Net-Str X)) ;
 j in X by A1, A3;
then reconsider y = j as Element of S ;
A11: Net-Str X is full SubRelStr of S by Th32;
 RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S, the InternalRel of S #) ;
then  f * (Net-Str X) is full SubRelStr of S by A1, A11, Th12;
then  y >= x by A10, YELLOW_0:59;
then  f . y >= f . x by WAYBEL_1:def_2;
hence  f . x <= z by A5, A9; ::_thesis: verum
end;
hence  H2(i) = f . i by A8, YELLOW_0:31; ::_thesis: verum
end;
  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  = f .: X
proof
thus   {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  c= f .: X :: according to XBOOLE_0:def_10 ::_thesis: f .: X c=  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  or x in f .: X )
assume  x in  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  ; ::_thesis: x in f .: X
then consider j being Element of (f * (Net-Str X)) such that
A12: x = H2(j) ;
reconsider j = j as Element of (f * (Net-Str X)) ;
A13: x = f . j by A6, A12;
 j in X by A1, A3;
hence  x in f .: X by A13, FUNCT_2:35; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  )
assume  y in f .: X ; ::_thesis: y in  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }
then consider x being set  such that
A14: x in the carrier of S and
A15: x in X and
A16: y = f . x by FUNCT_2:64;
reconsider x = x as Element of S by A14;
reconsider i = x as Element of (f * (Net-Str X)) by A1, A15, Th32;
 f . x = H2(i) by A6;
hence  y in  {  H2(j) where j is Element of (f * (Net-Str X)) : verum  }  by A16; ::_thesis: verum
end;
hence  lim_inf (f * (Net-Str X)) = sup (f .: X) by WAYBEL11:def_6; ::_thesis: verum
end;

theorem Th34: :: WAYBEL21:34
for S being non empty reflexive RelStr
for D being non empty directed Subset of S
for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )
proof
let S be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of S
for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )
let D be non empty directed Subset of S; ::_thesis: for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )
A1: dom (id D) = D ;
 rng (id D) = D ;
then reconsider g = id D as Function of D, the carrier of S by A1, FUNCT_2:def_1, RELSET_1:4;
 (id the carrier of S) | D = id D by FUNCT_3:1;
then  Net-Str D = Net-Str (D,g) by WAYBEL17:9;
hence  for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j ) by WAYBEL11:def_10; ::_thesis: verum
end;

theorem Th35: :: WAYBEL21:35
for T being complete Lawson TopLattice
for D being non empty directed Subset of T holds sup D in Lim (Net-Str D)
proof
let T be complete Lawson TopLattice; ::_thesis: for D being non empty directed Subset of T holds sup D in Lim (Net-Str D)
let D be non empty directed Subset of T; ::_thesis: sup D in Lim (Net-Str D)
set N = Net-Str D;
A1: the mapping of (Net-Str D) = id D by Th32;
A2: the carrier of (Net-Str D) = D by Th32;
set K = the prebasis of T;
now__::_thesis:_for_A_being_Subset_of_T_st_sup_D_in_A_&_A_in_the_prebasis_of_T_holds_
Net-Str_D_is_eventually_in_A
let A be Subset of T; ::_thesis: ( sup D in A & A in the prebasis of T implies Net-Str D is_eventually_in A )
assume A3: sup D in A ; ::_thesis: ( A in the prebasis of T implies Net-Str D is_eventually_in A )
A4: the prebasis of T c= the topology of T by TOPS_2:64;
assume  A in the prebasis of T ; ::_thesis: Net-Str D is_eventually_in A
then  A is open by A4, PRE_TOPC:def_2;
then  A is property(S) by WAYBEL19:36;
then consider y being Element of T such that
A5: y in D and
A6: for x being Element of T st x in D & x >= y holds
x in A by A3, WAYBEL11:def_3;
reconsider i = y as Element of (Net-Str D) by A5, Th32;
thus  Net-Str D is_eventually_in A ::_thesis: verum
proof
take  i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (Net-Str D) holds
( not i <= b1 or (Net-Str D) . b1 in A )
let j be Element of (Net-Str D); ::_thesis: ( not i <= j or (Net-Str D) . j in A )
A7: j = (Net-Str D) . j by A1, A2, FUNCT_1:17;
A8: y = (Net-Str D) . i by A1, A2, FUNCT_1:17;
assume  j >= i ; ::_thesis: (Net-Str D) . j in A
then  (Net-Str D) . j >= (Net-Str D) . i by Th34;
hence  (Net-Str D) . j in A by A2, A6, A7, A8; ::_thesis: verum
end;
end;
hence  sup D in Lim (Net-Str D) by WAYBEL19:25; ::_thesis: verum
end;

definition
let T be non empty 1-sorted ;
let N be net of T;
let M be non empty NetStr over T;
assume A1: M is subnet of N ;
mode Embedding of M,N ->  Function of M,N means :Def3: :: WAYBEL21:def 3
( the mapping of M = the mapping of N * it & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= it . p ) );
existence
 ex b1 being Function of M,N st
( the mapping of M = the mapping of N * b1 & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= b1 . p ) ) by A1, YELLOW_6:def_9;
end;

:: deftheorem Def3 defines Embedding WAYBEL21:def_3_:_
 for T being non empty 1-sorted
for N being net of T
for M being non empty NetStr over T st M is subnet of N holds
for b4 being Function of M,N holds
( b4 is Embedding of M,N iff ( the mapping of M = the mapping of N * b4 & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= b4 . p ) ) );

theorem Th36: :: WAYBEL21:36
for T being non empty 1-sorted
for N being net of T
for M being subnet of N
for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)
proof
let T be non empty 1-sorted ; ::_thesis: for N being net of T
for M being subnet of N
for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)
let N be net of T; ::_thesis: for M being subnet of N
for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)
let M be subnet of N; ::_thesis: for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)
let e be Embedding of M,N; ::_thesis: for i being Element of M holds M . i = N . (e . i)
let i be Element of M; ::_thesis: M . i = N . (e . i)
 the mapping of M = the mapping of N * e by Def3;
hence  M . i = N . (e . i) by FUNCT_2:15; ::_thesis: verum
end;

theorem Th37: :: WAYBEL21:37
for T being complete LATTICE
for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M
proof
let T be complete LATTICE; ::_thesis: for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M
let N be net of T; ::_thesis: for M being subnet of N holds lim_inf N <= lim_inf M
let M be subnet of N; ::_thesis: lim_inf N <= lim_inf M
deffunc H1( net of T) ->  set =  {  ("/\" ( {  ($1 . i) where i is Element of $1 : i >= j  }  ,T)) where j is Element of $1 : verum  }  ;
A1: "\/" (H1(M),T) is_>=_than H1(N)
proof
let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in H1(N) or t <= "\/" (H1(M),T) )
assume  t in H1(N) ; ::_thesis: t <= "\/" (H1(M),T)
then consider j being Element of N such that
A2: t = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,T) ;
set e = the Embedding of M,N;
reconsider j = j as Element of N ;
consider j9 being Element of M such that
A3: for p being Element of M st j9 <= p holds
j <= the Embedding of M,N . p by Def3;
set X =  {  (N . i) where i is Element of N : i >= j  }  ;
set Y =  {  (M . i) where i is Element of M : i >= j9  }  ;
A4: ex_inf_of  {  (N . i) where i is Element of N : i >= j  }  ,T by YELLOW_0:17;
A5: ex_inf_of  {  (M . i) where i is Element of M : i >= j9  }  ,T by YELLOW_0:17;
  {  (M . i) where i is Element of M : i >= j9  }  c=  {  (N . i) where i is Element of N : i >= j  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (M . i) where i is Element of M : i >= j9  }  or y in  {  (N . i) where i is Element of N : i >= j  }  )
assume  y in  {  (M . i) where i is Element of M : i >= j9  }  ; ::_thesis: y in  {  (N . i) where i is Element of N : i >= j  }
then consider i being Element of M such that
A6: y = M . i and
A7: i >= j9 ;
reconsider i = i as Element of M ;
 the Embedding of M,N . i >= j by A3, A7;
then  N . ( the Embedding of M,N . i) in  {  (N . i) where i is Element of N : i >= j  }  ;
hence  y in  {  (N . i) where i is Element of N : i >= j  }  by A6, Th36; ::_thesis: verum
end;
then A8: t <= "/\" ( {  (M . i) where i is Element of M : i >= j9  }  ,T) by A2, A4, A5, YELLOW_0:35;
 "/\" ( {  (M . i) where i is Element of M : i >= j9  }  ,T) in H1(M) ;
then  "/\" ( {  (M . i) where i is Element of M : i >= j9  }  ,T) <= "\/" (H1(M),T) by YELLOW_2:22;
hence  t <= "\/" (H1(M),T) by A8, YELLOW_0:def_2; ::_thesis: verum
end;
A9: lim_inf M = "\/" (H1(M),T) by WAYBEL11:def_6;
 lim_inf N = "\/" (H1(N),T) by WAYBEL11:def_6;
hence  lim_inf N <= lim_inf M by A1, A9, YELLOW_0:32; ::_thesis: verum
end;

theorem Th38: :: WAYBEL21:38
for T being complete LATTICE
for N being net of T
for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
proof
let T be complete LATTICE; ::_thesis: for N being net of T
for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
let N be net of T; ::_thesis: for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
let M be subnet of N; ::_thesis: for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
let e be Embedding of M,N; ::_thesis: ( ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) implies lim_inf N = lim_inf M )
assume A1: for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ; ::_thesis: lim_inf N = lim_inf M
deffunc H1( net of T) ->  set =  {  ("/\" ( {  ($1 . i) where i is Element of $1 : i >= j  }  ,T)) where j is Element of $1 : verum  }  ;
 "\/" (H1(N),T) is_>=_than H1(M)
proof
let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in H1(M) or t <= "\/" (H1(N),T) )
assume  t in H1(M) ; ::_thesis: t <= "\/" (H1(N),T)
then consider j being Element of M such that
A2: t = "/\" ( {  (M . i) where i is Element of M : i >= j  }  ,T) ;
reconsider j = j as Element of M ;
set j9 = e . j;
set X =  {  (N . i) where i is Element of N : i >= e . j  }  ;
set Y =  {  (M . i) where i is Element of M : i >= j  }  ;
 t is_<=_than  {  (N . i) where i is Element of N : i >= e . j  }
proof
let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in  {  (N . i) where i is Element of N : i >= e . j  }  or t <= x )
assume  x in  {  (N . i) where i is Element of N : i >= e . j  }  ; ::_thesis: t <= x
then consider i being Element of N such that
A3: x = N . i and
A4: i >= e . j ;
reconsider i = i as Element of N ;
consider k being Element of M such that
A5: k >= j and
A6: N . i >= M . k by A1, A4;
 M . k in  {  (M . i) where i is Element of M : i >= j  }  by A5;
then  M . k >= t by A2, YELLOW_2:22;
hence  t <= x by A3, A6, YELLOW_0:def_2; ::_thesis: verum
end;
then A7: t <= "/\" ( {  (N . i) where i is Element of N : i >= e . j  }  ,T) by YELLOW_0:33;
 "/\" ( {  (N . i) where i is Element of N : i >= e . j  }  ,T) in H1(N) ;
then  "/\" ( {  (N . i) where i is Element of N : i >= e . j  }  ,T) <= "\/" (H1(N),T) by YELLOW_2:22;
hence  t <= "\/" (H1(N),T) by A7, YELLOW_0:def_2; ::_thesis: verum
end;
then  "\/" (H1(N),T) >= "\/" (H1(M),T) by YELLOW_0:32;
then  lim_inf N >= "\/" (H1(M),T) by WAYBEL11:def_6;
then A8: lim_inf N >= lim_inf M by WAYBEL11:def_6;
 lim_inf M >= lim_inf N by Th37;
hence  lim_inf N = lim_inf M by A8, YELLOW_0:def_3; ::_thesis: verum
end;

theorem :: WAYBEL21:39
for T being non empty RelStr
for N being net of T
for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) holds
( M is subnet of N & incl (M,N) is Embedding of M,N )
proof
let T be non empty RelStr ; ::_thesis: for N being net of T
for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) holds
( M is subnet of N & incl (M,N) is Embedding of M,N )
let N be net of T; ::_thesis: for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) holds
( M is subnet of N & incl (M,N) is Embedding of M,N )
let M be non empty full SubNetStr of N; ::_thesis: ( ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) implies ( M is subnet of N & incl (M,N) is Embedding of M,N ) )
assume A1: for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ; ::_thesis: ( M is subnet of N & incl (M,N) is Embedding of M,N )
A2: the mapping of M = the mapping of N | the carrier of M by YELLOW_6:def_6;
A3: M is full SubRelStr of N by YELLOW_6:def_7;
then A4: the carrier of M c= the carrier of N by YELLOW_0:def_13;
 M is directed
proof
let x, y be Element of M; :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of M st
( x <= b1 & y <= b1 )
reconsider i = x, j = y as Element of N by A3, YELLOW_0:58;
consider k being Element of N such that
A5: k >= i and
A6: k >= j by YELLOW_6:def_3;
consider l being Element of N such that
A7: l >= k and
A8: l in the carrier of M by A1;
reconsider z = l as Element of M by A8;
take  z ; ::_thesis: ( x <= z & y <= z )
A9: l >= i by A5, A7, YELLOW_0:def_2;
 l >= j by A6, A7, YELLOW_0:def_2;
hence  ( x <= z & y <= z ) by A9, YELLOW_6:12; ::_thesis: verum
end;
then reconsider K = M as net of T by A3;
A10: now__::_thesis:_(_the_mapping_of_K_=_the_mapping_of_N_*_(incl_(K,N))_&_(_for_m_being_Element_of_N_ex_n_being_Element_of_K_st_
for_p_being_Element_of_K_st_n_<=_p_holds_
m_<=_(incl_(K,N))_._p_)_)
set f = incl (K,N);
A11: incl (K,N) = id the carrier of K by A4, YELLOW_9:def_1;
hence  the mapping of K = the mapping of N * (incl (K,N)) by A2, RELAT_1:65; ::_thesis: for m being Element of N ex n being Element of K st
for p being Element of K st n <= p holds
m <= (incl (K,N)) . p
let m be Element of N; ::_thesis: ex n being Element of K st
for p being Element of K st n <= p holds
m <= (incl (K,N)) . p
consider j being Element of N such that
A12: j >= m and
A13: j in the carrier of K by A1;
reconsider n = j as Element of K by A13;
take n = n; ::_thesis: for p being Element of K st n <= p holds
m <= (incl (K,N)) . p
let p be Element of K; ::_thesis: ( n <= p implies m <= (incl (K,N)) . p )
reconsider q = p as Element of N by A3, YELLOW_0:58;
assume  n <= p ; ::_thesis: m <= (incl (K,N)) . p
then A14: j <= q by YELLOW_6:11;
 (incl (K,N)) . p = q by A11, FUNCT_1:18;
hence  m <= (incl (K,N)) . p by A12, A14, YELLOW_0:def_2; ::_thesis: verum
end;
hence  M is subnet of N by YELLOW_6:def_9; ::_thesis: incl (M,N) is Embedding of M,N
hence  incl (M,N) is Embedding of M,N by A10, Def3; ::_thesis: verum
end;

theorem Th40: :: WAYBEL21:40
for T being non empty RelStr
for N being net of T
for i being Element of N holds
( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )
proof
let T be non empty RelStr ; ::_thesis: for N being net of T
for i being Element of N holds
( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )
let N be net of T; ::_thesis: for i being Element of N holds
( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )
let i be Element of N; ::_thesis: ( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )
set M = N | i;
set f = incl ((N | i),N);
thus  N | i is subnet of N ; ::_thesis: incl ((N | i),N) is Embedding of N | i,N
thus  N | i is subnet of N ; :: according to WAYBEL21:def_3 ::_thesis: ( the mapping of (N | i) = the mapping of N * (incl ((N | i),N)) & ( for m being Element of N ex n being Element of (N | i) st
for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p ) )
 N | i is full SubNetStr of N by WAYBEL_9:14;
then A1: N | i is full SubRelStr of N by YELLOW_6:def_7;
A2: incl ((N | i),N) = id the carrier of (N | i) by WAYBEL_9:13, YELLOW_9:def_1;
 the mapping of (N | i) = the mapping of N | the carrier of (N | i) by WAYBEL_9:def_7;
hence  the mapping of (N | i) = the mapping of N * (incl ((N | i),N)) by A2, RELAT_1:65; ::_thesis: for m being Element of N ex n being Element of (N | i) st
for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
let m be Element of N; ::_thesis: ex n being Element of (N | i) st
for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
consider n9 being Element of N such that
A3: n9 >= i and
A4: n9 >= m by YELLOW_6:def_3;
reconsider n = n9 as Element of (N | i) by A3, WAYBEL_9:def_7;
take  n ; ::_thesis: for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
let p be Element of (N | i); ::_thesis: ( n <= p implies m <= (incl ((N | i),N)) . p )
reconsider p9 = p as Element of N by A1, YELLOW_0:58;
assume  n <= p ; ::_thesis: m <= (incl ((N | i),N)) . p
then  n9 <= p9 by A1, YELLOW_0:59;
then  m <= p9 by A4, YELLOW_0:def_2;
hence  m <= (incl ((N | i),N)) . p by A2, FUNCT_1:18; ::_thesis: verum
end;

theorem Th41: :: WAYBEL21:41
for T being complete LATTICE
for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N
proof
let T be complete LATTICE; ::_thesis: for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N
let N be net of T; ::_thesis: for i being Element of N holds lim_inf (N | i) = lim_inf N
let i be Element of N; ::_thesis: lim_inf (N | i) = lim_inf N
reconsider M = N | i as subnet of N ;
reconsider e = incl (M,N) as Embedding of M,N by Th40;
 M is full SubNetStr of N by WAYBEL_9:14;
then A1: M is full SubRelStr of N by YELLOW_6:def_7;
A2: incl (M,N) = id the carrier of M by WAYBEL_9:13, YELLOW_9:def_1;
now__::_thesis:_for_k_being_Element_of_N
for_j_being_Element_of_M_st_e_._j_<=_k_holds_
ex_k9_being_Element_of_M_st_
(_k9_>=_j_&_N_._k_>=_M_._k9_)
let k be Element of N; ::_thesis: for j being Element of M st e . j <= k holds
ex k9 being Element of M st
( k9 >= j & N . k >= M . k9 )
let j be Element of M; ::_thesis: ( e . j <= k implies ex k9 being Element of M st
( k9 >= j & N . k >= M . k9 ) )
consider j9 being Element of N such that
A3: j9 = j and
A4: j9 >= i by WAYBEL_9:def_7;
assume  e . j <= k ; ::_thesis: ex k9 being Element of M st
( k9 >= j & N . k >= M . k9 )
then A5: k >= j9 by A2, A3, FUNCT_1:18;
then  k >= i by A4, YELLOW_0:def_2;
then reconsider k9 = k as Element of M by WAYBEL_9:def_7;
take k9 = k9; ::_thesis: ( k9 >= j & N . k >= M . k9 )
thus  k9 >= j by A1, A3, A5, YELLOW_0:60; ::_thesis: N . k >= M . k9
A6: M . k9 = N . (e . k9) by Th36;
 M . k9 <= M . k9 ;
hence  N . k >= M . k9 by A2, A6, FUNCT_1:18; ::_thesis: verum
end;
hence  lim_inf (N | i) = lim_inf N by Th38; ::_thesis: verum
end;

theorem Th42: :: WAYBEL21:42
for T being non empty RelStr
for N being net of T
for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
proof
let T be non empty RelStr ; ::_thesis: for N being net of T
for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
let N be net of T; ::_thesis: for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
let X be set ; ::_thesis: ( N is_eventually_in X implies ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X ) )
given i9 being Element of N such that A1: for j being Element of N st j >= i9 holds
N . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
 [#] N is directed by WAYBEL_0:def_6;
then consider i being Element of N such that
 i in [#] N and
A2: i9 <= i and
 i9 <= i by WAYBEL_0:def_1;
take  i ; ::_thesis: ( N . i in X & rng the mapping of (N | i) c= X )
thus  N . i in X by A1, A2; ::_thesis: rng the mapping of (N | i) c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the mapping of (N | i) or x in X )
assume  x in rng the mapping of (N | i) ; ::_thesis: x in X
then consider j being set  such that
A3: j in dom the mapping of (N | i) and
A4: x = the mapping of (N | i) . j by FUNCT_1:def_3;
A5: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def_1;
reconsider j = j as Element of (N | i) by A3;
 the carrier of (N | i) =  {  y where y is Element of N : i <= y  }  by WAYBEL_9:12;
then consider k being Element of N such that
A6: j = k and
A7: i <= k by A3, A5;
x = (N | i) . j by A4
.= N . k by A6, WAYBEL_9:16 ;
hence  x in X by A1, A2, A7, ORDERS_2:3; ::_thesis: verum
end;

theorem Th43: :: WAYBEL21:43
for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T
proof
let T be complete Lawson TopLattice; ::_thesis: for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T
let N be eventually-filtered net of T; ::_thesis: rng the mapping of N is non empty filtered Subset of T
reconsider F = rng the mapping of N as non empty Subset of T ;
 F is filtered
proof
let x, y be Element of T; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in F or not y in F or ex b1 being Element of the carrier of T st
( b1 in F & b1 <= x & b1 <= y ) )
assume  x in F ; ::_thesis: ( not y in F or ex b1 being Element of the carrier of T st
( b1 in F & b1 <= x & b1 <= y ) )
then consider i1 being set  such that
A1: i1 in dom the mapping of N and
A2: x = the mapping of N . i1 by FUNCT_1:def_3;
assume  y in F ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in F & b1 <= x & b1 <= y )
then consider i2 being set  such that
A3: i2 in dom the mapping of N and
A4: y = the mapping of N . i2 by FUNCT_1:def_3;
A5: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
reconsider i1 = i1, i2 = i2 as Element of N by A1, A3;
consider j1 being Element of N such that
A6: for k being Element of N st j1 <= k holds
N . i1 >= N . k by WAYBEL_0:12;
consider j2 being Element of N such that
A7: for k being Element of N st j2 <= k holds
N . i2 >= N . k by WAYBEL_0:12;
consider j being Element of N such that
A8: j2 <= j and
A9: j1 <= j by YELLOW_6:def_3;
take z = N . j; ::_thesis: ( z in F & z <= x & z <= y )
thus  z in F by A5, FUNCT_1:def_3; ::_thesis: ( z <= x & z <= y )
thus  ( z <= x & z <= y ) by A2, A4, A6, A7, A8, A9; ::_thesis: verum
end;
hence  rng the mapping of N is non empty filtered Subset of T ; ::_thesis: verum
end;

theorem Th44: :: WAYBEL21:44
for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds Lim N = {(inf N)}
proof
let T be complete Lawson TopLattice; ::_thesis: for N being eventually-filtered net of T holds Lim N = {(inf N)}
set S = the Scott TopAugmentation of T;
let N be eventually-filtered net of T; ::_thesis: Lim N = {(inf N)}
reconsider F = rng the mapping of N as non empty filtered Subset of T by Th43;
A1: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A3: inf N = Inf by WAYBEL_9:def_2
.= "/\" (F,T) by YELLOW_2:def_6 ;
A4: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
thus  Lim N c= {(inf N)} :: according to XBOOLE_0:def_10 ::_thesis: {(inf N)} c= Lim N
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Lim N or p in {(inf N)} )
assume A5: p in Lim N ; ::_thesis: p in {(inf N)}
then reconsider p = p as Element of T ;
 p is_<=_than F
proof
let u be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not u in F or p <= u )
assume  u in F ; ::_thesis: p <= u
then consider i being set  such that
A6: i in dom the mapping of N and
A7: u = the mapping of N . i by FUNCT_1:def_3;
reconsider i = i as Element of N by A6;
consider ii being Element of N such that
A8: for k being Element of N st ii <= k holds
N . i >= N . k by WAYBEL_0:12;
 downarrow u is closed by WAYBEL19:38;
then A9: Cl (downarrow u) = downarrow u by PRE_TOPC:22;
 N is_eventually_in downarrow u
proof
take  ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not ii <= b1 or N . b1 in downarrow u )
let j be Element of N; ::_thesis: ( not ii <= j or N . j in downarrow u )
assume  j >= ii ; ::_thesis: N . j in downarrow u
then  N . j <= N . i by A8;
hence  N . j in downarrow u by A7, WAYBEL_0:17; ::_thesis: verum
end;
then  Lim N c= downarrow u by A9, WAYBEL19:26;
hence  p <= u by A5, WAYBEL_0:17; ::_thesis: verum
end;
then A10: p <= inf N by A3, YELLOW_0:33;
 inf N is_<=_than F by A3, YELLOW_0:33;
then A11: F c= uparrow (inf N) by YELLOW_2:2;
 uparrow (inf N) is closed by WAYBEL19:38;
then  Cl (uparrow (inf N)) = uparrow (inf N) by PRE_TOPC:22;
then A12: Cl F c= uparrow (inf N) by A11, PRE_TOPC:19;
 p in Cl F by A5, WAYBEL_9:24;
then  p >= inf N by A12, WAYBEL_0:18;
then  p = inf N by A10, ORDERS_2:2;
hence  p in {(inf N)} by TARSKI:def_1; ::_thesis: verum
end;
reconsider K = (sigma T) \/  {  ((uparrow x) `) where x is Element of T : verum  }  as prebasis of T by WAYBEL19:30;
now__::_thesis:_for_A_being_Subset_of_T_st_inf_F_in_A_&_A_in_K_holds_
N_is_eventually_in_A
let A be Subset of T; ::_thesis: ( inf F in A & A in K implies N is_eventually_in b1 )
assume that
A13: inf F in A and
A14: A in K ; ::_thesis: N is_eventually_in b1
percases ( A in sigma T or A in  {  ((uparrow x) `) where x is Element of T : verum  }  ) by A14, XBOOLE_0:def_3;
supposeA15: A in sigma T ; ::_thesis: N is_eventually_in b1
then reconsider a = A as Subset of the Scott TopAugmentation of T by A1;
 a is open by A1, A15, PRE_TOPC:def_2;
then  a is upper by WAYBEL11:def_4;
then A16: A is upper by A2, WAYBEL_0:25;
set i = the Element of N;
thus  N is_eventually_in A ::_thesis: verum
proof
take  the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in A )
let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in A )
 N . j in F by A4, FUNCT_1:def_3;
then  N . j >= inf F by YELLOW_2:22;
hence  ( not the Element of N <= j or N . j in A ) by A13, A16, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
suppose A in  {  ((uparrow x) `) where x is Element of T : verum  }  ; ::_thesis: N is_eventually_in b1
then consider x being Element of T such that
A17: A = (uparrow x) ` ;
 not inf F >= x by A13, A17, YELLOW_9:1;
then  not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A18: y in F and
A19: not y >= x by LATTICE3:def_8;
consider i being set  such that
A20: i in the carrier of N and
A21: y = the mapping of N . i by A4, A18, FUNCT_1:def_3;
thus  N is_eventually_in A ::_thesis: verum
proof
reconsider i = i as Element of N by A20;
consider ii being Element of N such that
A22: for k being Element of N st ii <= k holds
N . i >= N . k by WAYBEL_0:12;
take  ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not ii <= b1 or N . b1 in A )
let j be Element of N; ::_thesis: ( not ii <= j or N . j in A )
assume  j >= ii ; ::_thesis: N . j in A
then  N . j <= N . i by A22;
then  not N . j >= x by A19, A21, ORDERS_2:3;
hence  N . j in A by A17, YELLOW_9:1; ::_thesis: verum
end;
end;
end;
end;
then  inf F in Lim N by WAYBEL19:25;
hence  {(inf N)} c= Lim N by A3, ZFMISC_1:31; ::_thesis: verum
end;

begin

theorem Th45: :: WAYBEL21:45
for S, T being complete Lawson TopLattice
for f being meet-preserving Function of S,T holds
( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
proof
let S, T be complete Lawson TopLattice; ::_thesis: for f being meet-preserving Function of S,T holds
( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
A1: [#] T <> {} ;
set Ss = the Scott TopAugmentation of S;
set Ts = the Scott TopAugmentation of T;
set Sl = the correct lower TopAugmentation of S;
set Tl = the correct lower TopAugmentation of T;
A2: S is TopAugmentation of S by YELLOW_9:44;
A3: T is TopAugmentation of T by YELLOW_9:44;
A4: S is Refinement of the Scott TopAugmentation of S, the correct lower TopAugmentation of S by A2, WAYBEL19:29;
A5: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by A3, WAYBEL19:29;
A6: T is TopAugmentation of the Scott TopAugmentation of T by YELLOW_9:45;
A7: S is TopAugmentation of the Scott TopAugmentation of S by YELLOW_9:45;
A8: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
A9: RelStr(# the carrier of the correct lower TopAugmentation of S, the InternalRel of the correct lower TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A11: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
let f be meet-preserving Function of S,T; ::_thesis: ( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
reconsider g = f as Function of the correct lower TopAugmentation of S, the correct lower TopAugmentation of T by A9, A11;
reconsider h = f as Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A8, A10;
A12: [#] the Scott TopAugmentation of T <> {} ;
hereby  ::_thesis: ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous )
assume A13: f is continuous ; ::_thesis: ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) )
now__::_thesis:_for_P_being_Subset_of_the_Scott_TopAugmentation_of_T_st_P_is_open_holds_
h_"_P_is_open
let P be Subset of the Scott TopAugmentation of T; ::_thesis: ( P is open implies h " P is open )
reconsider A = P as Subset of the Scott TopAugmentation of T ;
reconsider C = A as Subset of T by A10;
assume A14: P is open ; ::_thesis: h " P is open
then  C is open by A6, WAYBEL19:37;
then A15: f " C is open by A1, A13, TOPS_2:43;
 A is upper by A14, WAYBEL11:def_4;
then  h " A is upper by A8, A10, WAYBEL17:2, WAYBEL_9:1;
then  f " C is upper by A8, WAYBEL_0:25;
hence  h " P is open by A7, A15, WAYBEL19:41; ::_thesis: verum
end;
then  h is continuous by A12, TOPS_2:43;
hence  f is directed-sups-preserving by A8, A10, Th6; ::_thesis: for X being non empty Subset of S holds f preserves_inf_of X
 for X being non empty filtered Subset of S holds f preserves_inf_of X
proof
let F be non empty filtered Subset of S; ::_thesis: f preserves_inf_of F
assume  ex_inf_of F,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: F,T & "/\" ((f .: F),T) = f . ("/\" (F,S)) )
thus  ex_inf_of f .: F,T by YELLOW_0:17; ::_thesis: "/\" ((f .: F),T) = f . ("/\" (F,S))
 {(inf F)} = Lim (F opp+id) by WAYBEL19:43;
then  Im (f,(inf F)) c= Lim (f * (F opp+id)) by A13, Th24;
then  {(f . (inf F))} c= Lim (f * (F opp+id)) by SETWISEO:8;
then A16: f . (inf F) in Lim (f * (F opp+id)) by ZFMISC_1:31;
reconsider G = f .: F as non empty filtered Subset of T by WAYBEL20:24;
A17: rng the mapping of (f * (F opp+id)) = rng (f * the mapping of (F opp+id)) by WAYBEL_9:def_8
.= rng (f * (id F)) by WAYBEL19:27
.= rng (f | F) by RELAT_1:65
.= G by RELAT_1:115 ;
Lim (f * (F opp+id)) = {(inf (f * (F opp+id)))} by Th44
.= {(Inf )} by WAYBEL_9:def_2
.= {(inf G)} by A17, YELLOW_2:def_6 ;
hence  "/\" ((f .: F),T) = f . ("/\" (F,S)) by A16, TARSKI:def_1; ::_thesis: verum
end;
hence  for X being non empty Subset of S holds f preserves_inf_of X by Th4; ::_thesis: verum
end;
assume  f is directed-sups-preserving ; ::_thesis: ( ex X being non empty Subset of S st not f preserves_inf_of X or f is continuous )
then A18: h is directed-sups-preserving by A8, A10, Th6;
assume  for X being non empty Subset of S holds f preserves_inf_of X ; ::_thesis: f is continuous
then  for X being non empty Subset of the correct lower TopAugmentation of S holds g preserves_inf_of X by A9, A11, WAYBEL_0:65;
then  g is continuous by WAYBEL19:8;
hence  f is continuous by A4, A5, A18, WAYBEL19:24; ::_thesis: verum
end;

theorem Th46: :: WAYBEL21:46
for S, T being complete Lawson TopLattice
for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) )
proof
let S, T be complete Lawson TopLattice; ::_thesis: for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) )
let f be SemilatticeHomomorphism of S,T; ::_thesis: ( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) )
hereby  ::_thesis: ( f is infs-preserving & f is directed-sups-preserving implies f is continuous )
assume A1: f is continuous ; ::_thesis: ( f is infs-preserving & f is directed-sups-preserving )
A2: for X being finite Subset of S holds f preserves_inf_of X by Def1;
 for X being non empty filtered Subset of S holds f preserves_inf_of X by A1, Th45;
hence  f is infs-preserving by A2, WAYBEL_0:71; ::_thesis: f is directed-sups-preserving
thus  f is directed-sups-preserving by A1, Th45; ::_thesis: verum
end;
assume  f is infs-preserving ; ::_thesis: ( not f is directed-sups-preserving or f is continuous )
then  for X being non empty Subset of S holds f preserves_inf_of X by WAYBEL_0:def_32;
hence  ( not f is directed-sups-preserving or f is continuous ) by Th45; ::_thesis: verum
end;

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
attrf is lim_infs-preserving  means :: WAYBEL21:def 4
 for N being net of S holds f . (lim_inf N) = lim_inf (f * N);
end;

:: deftheorem  defines lim_infs-preserving WAYBEL21:def_4_:_
 for S, T being non empty RelStr
for f being Function of S,T holds
( f is lim_infs-preserving iff for N being net of S holds f . (lim_inf N) = lim_inf (f * N) );

theorem :: WAYBEL21:47
for S, T being complete Lawson TopLattice
for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff f is lim_infs-preserving )
proof
let S, T be complete Lawson TopLattice; ::_thesis: for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff f is lim_infs-preserving )
let f be SemilatticeHomomorphism of S,T; ::_thesis: ( f is continuous iff f is lim_infs-preserving )
thus  ( f is continuous implies f is lim_infs-preserving ) ::_thesis: ( f is lim_infs-preserving implies f is continuous )
proof
assume  f is continuous ; ::_thesis: f is lim_infs-preserving
then A1: ( f is infs-preserving & f is directed-sups-preserving ) by Th46;
let N be net of S; :: according to WAYBEL21:def_4 ::_thesis: f . (lim_inf N) = lim_inf (f * N)
set M = f * N;
set Y =  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  ;
reconsider X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  as non empty directed Subset of S by Th25;
A2: ex_sup_of X,S by YELLOW_0:17;
A3: f preserves_sup_of X by A1, WAYBEL_0:def_37;
A4: 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;
A5: the carrier of S c= dom f by FUNCT_2:def_1;
deffunc H1( Element of N) ->  set =  {  (N . i) where i is Element of N : i >= $1  }  ;
deffunc H2( Element of N) ->  Element of the carrier of S = "/\" (H1($1),S);
defpred S1[ set ] means verum;
A6: f .:  {  H2(i) where i is Element of N : S1[i]  }  =  {  (f . H2(i)) where i is Element of N : S1[i]  }  from LATTICE3:sch_2(A5);
A7: f .: X =  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }
proof
A8: now__::_thesis:_for_j_being_Element_of_N
for_j9_being_Element_of_(f_*_N)_st_j9_=_j_holds_
f_.:_H1(j)_=__{__((f_*_N)_._n)_where_n_is_Element_of_(f_*_N)_:_n_>=_j9__}_
let j be Element of N; ::_thesis: for j9 being Element of (f * N) st j9 = j holds
f .: H1(j) =  {  ((f * N) . n) where n is Element of (f * N) : n >= j9  }
let j9 be Element of (f * N); ::_thesis: ( j9 = j implies f .: H1(j) =  {  ((f * N) . n) where n is Element of (f * N) : n >= j9  }  )
assume A9: j9 = j ; ::_thesis: f .: H1(j) =  {  ((f * N) . n) where n is Element of (f * N) : n >= j9  }
defpred S2[ Element of N] means $1 >= j;
defpred S3[ Element of (f * N)] means $1 >= j9;
deffunc H3( Element of N) ->  Element of the carrier of T = f . (N . $1);
deffunc H4( set ) ->  set = f . ( the mapping of N . $1);
A10: for v being Element of N st S2[v] holds
H3(v) = H4(v) ;
deffunc H5( set ) ->  set = (f * the mapping of N) . $1;
deffunc H6( Element of (f * N)) ->  Element of the carrier of T = (f * N) . $1;
A11: for v being Element of N st S2[v] holds
H4(v) = H5(v) by FUNCT_2:15;
A12: for v being Element of (f * N) st S3[v] holds
H5(v) = H6(v) by WAYBEL_9:def_8;
defpred S4[ set ] means [j9,$1] in the InternalRel of N;
A13: for v being Element of N holds
( S2[v] iff S4[v] ) by A9, ORDERS_2:def_5;
A14: for v being Element of (f * N) holds
( S4[v] iff S3[v] ) by A4, ORDERS_2:def_5;
deffunc H7( Element of N) ->  Element of the carrier of S = N . $1;
thus f .: H1(j) = f .:  {  H7(i) where i is Element of N : S2[i]  }
.=  {  (f . H7(k)) where k is Element of N : S2[k]  }  from LATTICE3:sch_2(A5)
.=  {  H3(k) where k is Element of N : S2[k]  }
.=  {  H4(s) where s is Element of N : S2[s]  }  from FRAENKEL:sch_6(A10)
.=  {  H5(o) where o is Element of N : S2[o]  }  from FRAENKEL:sch_6(A11)
.=  {  H5(r) where r is Element of N : S4[r]  }  from FRAENKEL:sch_3(A13)
.=  {  H5(m) where m is Element of (f * N) : S4[m]  }  by A4
.=  {  H5(q) where q is Element of (f * N) : S3[q]  }  from FRAENKEL:sch_3(A14)
.=  {  H6(n) where n is Element of (f * N) : S3[n]  }  from FRAENKEL:sch_6(A12)
.=  {  ((f * N) . n) where n is Element of (f * N) : n >= j9  }  ; ::_thesis: verum
end;
A15: now__::_thesis:_for_j_being_Element_of_N_holds_f_._("/\"_(H1(j),S))_=_"/\"_((f_.:_H1(j)),T)
let j be Element of N; ::_thesis: f . ("/\" (H1(j),S)) = "/\" ((f .: H1(j)),T)
 H1(j) c= the carrier of S
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in H1(j) or b in the carrier of S )
assume  b in H1(j) ; ::_thesis: b in the carrier of S
then  ex i being Element of N st
( b = N . i & i >= j ) ;
hence  b in the carrier of S ; ::_thesis: verum
end;
then reconsider A = H1(j) as Subset of S ;
A16: f preserves_inf_of A by A1, WAYBEL_0:def_32;
 ex_inf_of A,S by YELLOW_0:17;
hence  f . ("/\" (H1(j),S)) = "/\" ((f .: H1(j)),T) by A16, WAYBEL_0:def_30; ::_thesis: verum
end;
thus  f .: X c=  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  c= f .: X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: X or a in  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  )
assume  a in f .: X ; ::_thesis: a in  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }
then consider j being Element of N such that
A17: a = f . ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) by A6;
A18: a = "/\" ((f .: H1(j)),T) by A15, A17;
reconsider j9 = j as Element of (f * N) by A4;
 f .: H1(j) =  {  ((f * N) . n) where n is Element of (f * N) : n >= j9  }  by A8;
hence  a in  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  by A18; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  or a in f .: X )
assume  a in  {  ("/\" ( {  ((f * N) . i) where i is Element of (f * N) : i >= j  }  ,T)) where j is Element of (f * N) : verum  }  ; ::_thesis: a in f .: X
then consider j9 being Element of (f * N) such that
A19: a = "/\" ( {  ((f * N) . n) where n is Element of (f * N) : n >= j9  }  ,T) ;
reconsider j = j9 as Element of N by A4;
a = "/\" ((f .: H1(j)),T) by A8, A19
.= f . ("/\" (H1(j),S)) by A15 ;
hence  a in f .: X by A6; ::_thesis: verum
end;
thus f . (lim_inf N) = f . (sup X) by WAYBEL11:def_6
.= sup (f .: X) by A2, A3, WAYBEL_0:def_31
.= lim_inf (f * N) by A7, WAYBEL11:def_6 ; ::_thesis: verum
end;
assume A20: for N being net of S holds f . (lim_inf N) = lim_inf (f * N) ; :: according to WAYBEL21:def_4 ::_thesis: f is continuous
A21: f is directed-sups-preserving
proof
let D be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or f preserves_sup_of D )
assume  ( not D is empty & D is directed ) ; ::_thesis: f preserves_sup_of D
then reconsider D9 = D as non empty directed Subset of S ;
assume  ex_sup_of D,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: D,T & "\/" ((f .: D),T) = f . ("\/" (D,S)) )
thus  ex_sup_of f .: D,T by YELLOW_0:17; ::_thesis: "\/" ((f .: D),T) = f . ("\/" (D,S))
thus f . (sup D) = f . (lim_inf (Net-Str D9)) by WAYBEL17:10
.= lim_inf (f * (Net-Str D9)) by A20
.= sup (f .: D) by Th33 ; ::_thesis: verum
end;
A22: for X being finite Subset of S holds f preserves_inf_of X by Def1;
now__::_thesis:_for_X_being_non_empty_filtered_Subset_of_S_holds_f_preserves_inf_of_X
let X be non empty filtered Subset of S; ::_thesis: f preserves_inf_of X
reconsider fX = f .: X as non empty filtered Subset of T by WAYBEL20:24;
thus  f preserves_inf_of X ::_thesis: verum
proof
assume  ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
thus  ex_inf_of f .: X,T by YELLOW_0:17; ::_thesis: "/\" ((f .: X),T) = f . ("/\" (X,S))
f . (inf X) = f . (lim_inf (X opp+id)) by Th28
.= lim_inf (f * (X opp+id)) by A20
.= inf fX by Th29
.= lim_inf (fX opp+id) by Th28 ;
hence  "/\" ((f .: X),T) = f . ("/\" (X,S)) by Th28; ::_thesis: verum
end;
end;
then  f is infs-preserving by A22, WAYBEL_0:71;
hence  f is continuous by A21, Th46; ::_thesis: verum
end;

theorem Th48: :: WAYBEL21:48
for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is infs-inheriting
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is infs-inheriting
let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: ( Top T in the carrier of S & ex X being Subset of T st
( X = the carrier of S & X is closed ) implies S is infs-inheriting )
assume A1: Top T in the carrier of S ; ::_thesis: ( for X being Subset of T holds
( not X = the carrier of S or not X is closed ) or S is infs-inheriting )
given X being Subset of T such that A2: X = the carrier of S and
A3: X is closed ; ::_thesis: S is infs-inheriting
 S is filtered-infs-inheriting
proof
let Y be filtered Subset of S; :: according to WAYBEL_0:def_3 ::_thesis: ( Y = {} or not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
assume  Y <> {} ; ::_thesis: ( not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
then reconsider F = Y as non empty filtered Subset of T by YELLOW_2:7;
set N = F opp+id ;
assume  ex_inf_of Y,T ; ::_thesis: "/\" (Y,T) in the carrier of S
 the mapping of (F opp+id) = id Y by WAYBEL19:27;
then A4: rng the mapping of (F opp+id) = Y by RELAT_1:45;
 Lim (F opp+id) = {(inf F)} by WAYBEL19:43;
then  {(inf F)} c= Cl X by A2, A4, Th27, WAYBEL19:26;
then  {(inf F)} c= X by A3, PRE_TOPC:22;
hence  "/\" (Y,T) in the carrier of S by A2, ZFMISC_1:31; ::_thesis: verum
end;
hence  S is infs-inheriting by A1, Th16; ::_thesis: verum
end;

theorem Th49: :: WAYBEL21:49
for T being continuous complete Lawson TopLattice
for S being non empty full SubRelStr of T st ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is directed-sups-inheriting
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full SubRelStr of T st ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is directed-sups-inheriting
let S be non empty full SubRelStr of T; ::_thesis: ( ex X being Subset of T st
( X = the carrier of S & X is closed ) implies S is directed-sups-inheriting )
given X being Subset of T such that A1: X = the carrier of S and
A2: X is closed ; ::_thesis: S is directed-sups-inheriting
let Y be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( Y = {} or not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S )
assume  Y <> {} ; ::_thesis: ( not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S )
then reconsider D = Y as non empty directed Subset of T by YELLOW_2:7;
set N = Net-Str D;
assume  ex_sup_of Y,T ; ::_thesis: "\/" (Y,T) in the carrier of S
 the mapping of (Net-Str D) = id Y by Th32;
then  rng the mapping of (Net-Str D) = Y by RELAT_1:45;
then  Lim (Net-Str D) c= Cl X by A1, Th27, WAYBEL19:26;
then A3: Lim (Net-Str D) c= X by A2, PRE_TOPC:22;
 sup D in Lim (Net-Str D) by Th35;
hence  "\/" (Y,T) in the carrier of S by A1, A3; ::_thesis: verum
end;

theorem Th50: :: WAYBEL21:50
for T being continuous complete Lawson TopLattice
for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st
( X = the carrier of S & X is closed )
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st
( X = the carrier of S & X is closed )
let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; ::_thesis: ex X being Subset of T st
( X = the carrier of S & X is closed )
reconsider X = the carrier of S as Subset of T by YELLOW_0:def_13;
take  X ; ::_thesis: ( X = the carrier of S & X is closed )
thus  X = the carrier of S ; ::_thesis: X is closed
reconsider S = S as complete CLSubFrame of T by Th18;
set SL = the correct Lawson TopAugmentation of S;
A1: RelStr(# the carrier of the correct Lawson TopAugmentation of S, the InternalRel of the correct Lawson TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
set f = incl ( the correct Lawson TopAugmentation of S,T);
set f9 = incl (S,T);
A2: the carrier of S c= the carrier of T by YELLOW_0:def_13;
then A3: incl ( the correct Lawson TopAugmentation of S,T) = id the carrier of the correct Lawson TopAugmentation of S by A1, YELLOW_9:def_1;
A4: incl (S,T) = id the carrier of the correct Lawson TopAugmentation of S by A1, A2, YELLOW_9:def_1;
A5: [#] the correct Lawson TopAugmentation of S is compact by COMPTS_1:1;
A6: incl (S,T) is infs-preserving by Th8;
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T, the InternalRel of T #) ;
then A7: ( incl ( the correct Lawson TopAugmentation of S,T) is infs-preserving & incl ( the correct Lawson TopAugmentation of S,T) is directed-sups-preserving ) by A1, A3, A4, A6, Th6, Th10;
then  incl ( the correct Lawson TopAugmentation of S,T) is SemilatticeHomomorphism of the correct Lawson TopAugmentation of S,T by Th5;
then  incl ( the correct Lawson TopAugmentation of S,T) is continuous by A7, Th46;
then  (incl ( the correct Lawson TopAugmentation of S,T)) .: ([#] the correct Lawson TopAugmentation of S) is compact by A5, WEIERSTR:8;
then  X is compact by A1, A3, FUNCT_1:92;
hence  X is closed by COMPTS_1:7; ::_thesis: verum
end;

theorem Th51: :: WAYBEL21:51
for T being continuous complete Lawson TopLattice
for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T
for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T
for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S
let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; ::_thesis: for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S
set X = the carrier of S;
let N be net of T; ::_thesis: ( N is_eventually_in the carrier of S implies lim_inf N in the carrier of S )
assume  N is_eventually_in the carrier of S ; ::_thesis: lim_inf N in the carrier of S
then consider a being Element of N such that
 N . a in the carrier of S and
A1: rng the mapping of (N | a) c= the carrier of S by Th42;
deffunc H1( Element of (N | a)) ->  set =  {  ((N | a) . i) where i is Element of (N | a) : i >= $1  }  ;
reconsider iN =  {  ("/\" (H1(j),T)) where j is Element of (N | a) : verum  }  as non empty directed Subset of T by Th25;
 iN c= the carrier of S
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in iN or z in the carrier of S )
assume  z in iN ; ::_thesis: z in the carrier of S
then consider j being Element of (N | a) such that
A2: z = "/\" (H1(j),T) ;
 H1(j) c= the carrier of S
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in H1(j) or u in the carrier of S )
assume  u in H1(j) ; ::_thesis: u in the carrier of S
then  ex i being Element of (N | a) st
( u = (N | a) . i & i >= j ) ;
then  u in rng the mapping of (N | a) by FUNCT_2:4;
hence  u in the carrier of S by A1; ::_thesis: verum
end;
then reconsider Xj = H1(j) as Subset of S ;
 ex_inf_of Xj,T by YELLOW_0:17;
hence  z in the carrier of S by A2, YELLOW_0:def_18; ::_thesis: verum
end;
then reconsider jN = iN as non empty Subset of S ;
A3: jN is directed by WAYBEL10:23;
 ex_sup_of jN,T by YELLOW_0:17;
then  "\/" (jN,T) in the carrier of S by A3, WAYBEL_0:def_4;
then  lim_inf (N | a) in the carrier of S by WAYBEL11:def_6;
hence  lim_inf N in the carrier of S by Th41; ::_thesis: verum
end;

theorem Th52: :: WAYBEL21:52
for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is infs-inheriting
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is infs-inheriting
let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: ( Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) implies S is infs-inheriting )
assume A1: Top T in the carrier of S ; ::_thesis: ( ex N being net of T st
( rng the mapping of N c= the carrier of S & not lim_inf N in the carrier of S ) or S is infs-inheriting )
set X = the carrier of S;
assume A2: for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ; ::_thesis: S is infs-inheriting
 S is filtered-infs-inheriting
proof
let Y be filtered Subset of S; :: according to WAYBEL_0:def_3 ::_thesis: ( Y = {} or not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
assume  Y <> {} ; ::_thesis: ( not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
then reconsider F = Y as non empty filtered Subset of T by YELLOW_2:7;
assume  ex_inf_of Y,T ; ::_thesis: "/\" (Y,T) in the carrier of S
 the mapping of (F opp+id) = id F by WAYBEL19:27;
then A3: rng the mapping of (F opp+id) = Y by RELAT_1:45;
 lim_inf (F opp+id) = inf F by Th28;
hence  "/\" (Y,T) in the carrier of S by A2, A3; ::_thesis: verum
end;
hence  S is infs-inheriting by A1, Th16; ::_thesis: verum
end;

theorem Th53: :: WAYBEL21:53
for T being continuous complete Lawson TopLattice
for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is directed-sups-inheriting
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is directed-sups-inheriting
let S be non empty full SubRelStr of T; ::_thesis: ( ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) implies S is directed-sups-inheriting )
set X = the carrier of S;
assume A1: for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ; ::_thesis: S is directed-sups-inheriting
let Y be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( Y = {} or not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S )
assume  Y <> {} ; ::_thesis: ( not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S )
then reconsider F = Y as non empty directed Subset of T by YELLOW_2:7;
assume  ex_sup_of Y,T ; ::_thesis: "\/" (Y,T) in the carrier of S
 the mapping of (Net-Str F) = id F by Th32;
then A2: rng the mapping of (Net-Str F) = Y by RELAT_1:45;
 lim_inf (Net-Str F) = sup F by WAYBEL17:10;
hence  "\/" (Y,T) in the carrier of S by A1, A2; ::_thesis: verum
end;

theorem :: WAYBEL21:54
for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T
for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
proof
let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T
for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
let X be Subset of T; ::_thesis: ( X = the carrier of S & Top T in X implies ( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X ) )
assume that
A1: X = the carrier of S and
A2: Top T in X ; ::_thesis: ( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
hereby  ::_thesis: ( ( for N being net of T st N is_eventually_in X holds
lim_inf N in X ) implies X is closed )
assume  X is closed ; ::_thesis: for N being net of T st N is_eventually_in X holds
lim_inf N in X
then  S is non empty full infs-inheriting directed-sups-inheriting SubRelStr of T by A1, A2, Th48, Th49;
hence  for N being net of T st N is_eventually_in X holds
lim_inf N in X by A1, Th51; ::_thesis: verum
end;
assume  for N being net of T st N is_eventually_in X holds
lim_inf N in X ; ::_thesis: X is closed
then  for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S by A1, Th27;
then  ( S is infs-inheriting & S is directed-sups-inheriting ) by A1, A2, Th52, Th53;
then  ex X being Subset of T st
( X = the carrier of S & X is closed ) by Th50;
hence  X is closed by A1; ::_thesis: verum
end;