:: WAYBEL23 semantic presentation

begin

theorem Th1: :: WAYBEL23:1
for L being non empty Poset
for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
proof
let L be non empty Poset; ::_thesis: for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
let x be Element of L; ::_thesis: compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
A1: compactbelow x c= (waybelow x) /\ the carrier of (CompactSublatt L)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in compactbelow x or y in (waybelow x) /\ the carrier of (CompactSublatt L) )
assume A2: y in compactbelow x ; ::_thesis: y in (waybelow x) /\ the carrier of (CompactSublatt L)
then reconsider y1 = y as Element of L ;
A3: y in (downarrow x) /\ the carrier of (CompactSublatt L) by A2, WAYBEL_8:5;
then  y in downarrow x by XBOOLE_0:def_4;
then A4: y1 <= x by WAYBEL_0:17;
A5: y in the carrier of (CompactSublatt L) by A3, XBOOLE_0:def_4;
then  y1 is compact by WAYBEL_8:def_1;
then  y1 << y1 by WAYBEL_3:def_2;
then  y1 << x by A4, WAYBEL_3:2;
then  y1 in waybelow x by WAYBEL_3:7;
hence  y in (waybelow x) /\ the carrier of (CompactSublatt L) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
 (waybelow x) /\ the carrier of (CompactSublatt L) c= compactbelow x
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (waybelow x) /\ the carrier of (CompactSublatt L) or y in compactbelow x )
assume A6: y in (waybelow x) /\ the carrier of (CompactSublatt L) ; ::_thesis: y in compactbelow x
then reconsider y1 = y as Element of L ;
 y in waybelow x by A6, XBOOLE_0:def_4;
then  y1 << x by WAYBEL_3:7;
then  y1 <= x by WAYBEL_3:1;
then A7: y in downarrow x by WAYBEL_0:17;
 y in the carrier of (CompactSublatt L) by A6, XBOOLE_0:def_4;
then  y in (downarrow x) /\ the carrier of (CompactSublatt L) by A7, XBOOLE_0:def_4;
hence  y in compactbelow x by WAYBEL_8:5; ::_thesis: verum
end;
hence  compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let L be non empty reflexive transitive RelStr ;
let X be Subset of (InclPoset (Ids L));
:: original: union
redefine func union X ->  Subset of L;
coherence
 union X is Subset of L
proof
 union X c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in the carrier of L )
assume  x in union X ; ::_thesis: x in the carrier of L
then consider Y being set  such that
A1: x in Y and
A2: Y in X by TARSKI:def_4;
reconsider Y = Y as Ideal of L by A2, YELLOW_2:41;
 x in Y by A1;
hence  x in the carrier of L ; ::_thesis: verum
end;
hence  union X is Subset of L ; ::_thesis: verum
end;
end;

Lm1:  for X being non empty set
for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
proof
let X be non empty set ; ::_thesis: for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
let Y be Subset of (InclPoset X); ::_thesis: ( ex_sup_of Y, InclPoset X implies union Y c= sup Y )
assume A1: ex_sup_of Y, InclPoset X ; ::_thesis: union Y c= sup Y
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
x_c=_sup_Y
let x be set ; ::_thesis: ( x in Y implies x c= sup Y )
assume A2: x in Y ; ::_thesis: x c= sup Y
then reconsider x1 = x as Element of (InclPoset X) ;
 sup Y is_>=_than Y by A1, YELLOW_0:30;
then  sup Y >= x1 by A2, LATTICE3:def_9;
hence  x c= sup Y by YELLOW_1:3; ::_thesis: verum
end;
hence  union Y c= sup Y by ZFMISC_1:76; ::_thesis: verum
end;

theorem Th2: :: WAYBEL23:2
for L being non empty RelStr
for X, Y being Subset of L st X c= Y holds
finsups X c= finsups Y
proof
let L be non empty RelStr ; ::_thesis: for X, Y being Subset of L st X c= Y holds
finsups X c= finsups Y
let X, Y be Subset of L; ::_thesis: ( X c= Y implies finsups X c= finsups Y )
assume A1: X c= Y ; ::_thesis: finsups X c= finsups Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups X or x in finsups Y )
assume  x in finsups X ; ::_thesis: x in finsups Y
then  x in  {  ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L  }  by WAYBEL_0:def_27;
then consider Z being finite Subset of X such that
A2: x = "\/" (Z,L) and
A3: ex_sup_of Z,L ;
reconsider Z = Z as finite Subset of Y by A1, XBOOLE_1:1;
 ex_sup_of Z,L by A3;
then  x in  {  ("\/" (V,L)) where V is finite Subset of Y : ex_sup_of V,L  }  by A2;
hence  x in finsups Y by WAYBEL_0:def_27; ::_thesis: verum
end;

theorem Th3: :: WAYBEL23:3
for L being non empty transitive RelStr
for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y
let S be non empty full sups-inheriting SubRelStr of L; ::_thesis: for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y
let X be Subset of L; ::_thesis: for Y being Subset of S st X = Y holds
finsups X c= finsups Y
let Y be Subset of S; ::_thesis: ( X = Y implies finsups X c= finsups Y )
assume A1: X = Y ; ::_thesis: finsups X c= finsups Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups X or x in finsups Y )
assume  x in finsups X ; ::_thesis: x in finsups Y
then  x in  {  ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L  }  by WAYBEL_0:def_27;
then consider Z being finite Subset of X such that
A2: x = "\/" (Z,L) and
A3: ex_sup_of Z,L ;
reconsider Z = Z as finite Subset of Y by A1;
reconsider Z1 = Z as Subset of S by XBOOLE_1:1;
A4: "\/" (Z1,L) in the carrier of S by A3, YELLOW_0:def_19;
then A5: ex_sup_of Z1,S by A3, YELLOW_0:64;
 x = "\/" (Z1,S) by A2, A3, A4, YELLOW_0:64;
then  x in  {  ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S  }  by A5;
hence  x in finsups Y by WAYBEL_0:def_27; ::_thesis: verum
end;

theorem :: WAYBEL23:4
for L being non empty transitive antisymmetric complete RelStr
for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X = finsups Y
proof
let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X = finsups Y
let S be non empty full sups-inheriting SubRelStr of L; ::_thesis: for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X = finsups Y
let X be Subset of L; ::_thesis: for Y being Subset of S st X = Y holds
finsups X = finsups Y
let Y be Subset of S; ::_thesis: ( X = Y implies finsups X = finsups Y )
assume A1: X = Y ; ::_thesis: finsups X = finsups Y
hence  finsups X c= finsups Y by Th3; :: according to XBOOLE_0:def_10 ::_thesis: finsups Y c= finsups X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups Y or x in finsups X )
assume  x in finsups Y ; ::_thesis: x in finsups X
then  x in  {  ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S  }  by WAYBEL_0:def_27;
then consider Z being finite Subset of Y such that
A2: x = "\/" (Z,S) and
 ex_sup_of Z,S ;
reconsider Z = Z as finite Subset of X by A1;
reconsider Z1 = Z as Subset of S by XBOOLE_1:1;
A3: ex_sup_of Z1,L by YELLOW_0:17;
then  "\/" (Z1,L) in the carrier of S by YELLOW_0:def_19;
then  x = "\/" (Z1,L) by A2, A3, YELLOW_0:64;
then  x in  {  ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L  }  by A3;
hence  x in finsups X by WAYBEL_0:def_27; ::_thesis: verum
end;

theorem Th5: :: WAYBEL23:5
for L being complete sup-Semilattice
for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups Y c= finsups X
proof
let L be complete sup-Semilattice; ::_thesis: for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups Y c= finsups X
let S be non empty full join-inheriting SubRelStr of L; ::_thesis: ( Bottom L in the carrier of S implies for X being Subset of L
for Y being Subset of S st X = Y holds
finsups Y c= finsups X )
assume A1: Bottom L in the carrier of S ; ::_thesis: for X being Subset of L
for Y being Subset of S st X = Y holds
finsups Y c= finsups X
let X be Subset of L; ::_thesis: for Y being Subset of S st X = Y holds
finsups Y c= finsups X
let Y be Subset of S; ::_thesis: ( X = Y implies finsups Y c= finsups X )
assume A2: X = Y ; ::_thesis: finsups Y c= finsups X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups Y or x in finsups X )
assume  x in finsups Y ; ::_thesis: x in finsups X
then  x in  {  ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S  }  by WAYBEL_0:def_27;
then consider Z being finite Subset of Y such that
A3: x = "\/" (Z,S) and
A4: ex_sup_of Z,S ;
reconsider Z = Z as finite Subset of X by A2;
now__::_thesis:_x_in_finsups_X
percases ( not Z is empty or Z is empty ) ;
suppose not Z is empty ; ::_thesis: x in finsups X
then reconsider Z1 = Z as non empty finite Subset of S by XBOOLE_1:1;
reconsider xl = "\/" (Z1,L) as Element of S by WAYBEL21:15;
A5: ex_sup_of Z1,L by YELLOW_0:17;
A6: now__::_thesis:_for_b_being_Element_of_S_st_b_is_>=_than_Z1_holds_
xl_<=_b
let b be Element of S; ::_thesis: ( b is_>=_than Z1 implies xl <= b )
reconsider b1 = b as Element of L by YELLOW_0:58;
assume A7: b is_>=_than Z1 ; ::_thesis: xl <= b
 b1 is_>=_than Z1
proof
let c1 be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c1 in Z1 or c1 <= b1 )
assume A8: c1 in Z1 ; ::_thesis: c1 <= b1
then reconsider c = c1 as Element of S ;
 c <= b by A7, A8, LATTICE3:def_9;
hence  c1 <= b1 by YELLOW_0:59; ::_thesis: verum
end;
then  "\/" (Z1,L) <= b1 by A5, YELLOW_0:30;
hence  xl <= b by YELLOW_0:60; ::_thesis: verum
end;
A9: "\/" (Z1,L) is_>=_than Z1 by A5, YELLOW_0:30;
 xl is_>=_than Z1
proof
let b be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not b in Z1 or b <= xl )
reconsider b1 = b as Element of L by YELLOW_0:58;
assume  b in Z1 ; ::_thesis: b <= xl
then  b1 <= "\/" (Z1,L) by A9, LATTICE3:def_9;
hence  b <= xl by YELLOW_0:60; ::_thesis: verum
end;
then  "\/" (Z1,S) = "\/" (Z1,L) by A6, YELLOW_0:30;
then  x in  {  ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L  }  by A3, A5;
hence  x in finsups X by WAYBEL_0:def_27; ::_thesis: verum
end;
supposeA10: Z is empty ; ::_thesis: x in finsups X
reconsider dL = Bottom L as Element of S by A1;
reconsider dS = Bottom S as Element of L by YELLOW_0:58;
 S is lower-bounded by A4, A10, WAYBEL20:6;
then  Bottom S <= dL by YELLOW_0:44;
then A11: dS <= Bottom L by YELLOW_0:59;
A12: ex_sup_of Z,L by YELLOW_0:17;
 Bottom L <= dS by YELLOW_0:44;
then  dS = Bottom L by A11, YELLOW_0:def_3;
then  x in  {  ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L  }  by A3, A10, A12;
hence  x in finsups X by WAYBEL_0:def_27; ::_thesis: verum
end;
end;
end;
hence  x in finsups X ; ::_thesis: verum
end;

theorem Th6: :: WAYBEL23:6
for L being lower-bounded sup-Semilattice
for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))
let X be Subset of (InclPoset (Ids L)); ::_thesis: sup X = downarrow (finsups (union X))
reconsider a = downarrow (finsups (union X)) as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A1: union X c= sup X by Lm1, YELLOW_0:17;
A2: now__::_thesis:_for_b_being_Element_of_(InclPoset_(Ids_L))_st_b_is_>=_than_X_holds_
a_<=_b
let b be Element of (InclPoset (Ids L)); ::_thesis: ( b is_>=_than X implies a <= b )
reconsider b1 = b as Ideal of L by YELLOW_2:41;
assume  b is_>=_than X ; ::_thesis: a <= b
then  b >= sup X by YELLOW_0:32;
then  sup X c= b1 by YELLOW_1:3;
then  union X c= b1 by A1, XBOOLE_1:1;
then  downarrow (finsups (union X)) c= b1 by WAYBEL_0:61;
hence  a <= b by YELLOW_1:3; ::_thesis: verum
end;
A3: union X c= downarrow (finsups (union X)) by WAYBEL_0:61;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Ids_L))_st_b_in_X_holds_
b_<=_a
let b be Element of (InclPoset (Ids L)); ::_thesis: ( b in X implies b <= a )
assume  b in X ; ::_thesis: b <= a
then  b c= union X by ZFMISC_1:74;
then  b c= downarrow (finsups (union X)) by A3, XBOOLE_1:1;
hence  b <= a by YELLOW_1:3; ::_thesis: verum
end;
then  a is_>=_than X by LATTICE3:def_9;
hence  sup X = downarrow (finsups (union X)) by A2, YELLOW_0:32; ::_thesis: verum
end;

theorem Th7: :: WAYBEL23:7
for L being reflexive transitive RelStr
for X being Subset of L holds downarrow (downarrow X) = downarrow X
proof
let L be reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds downarrow (downarrow X) = downarrow X
let X be Subset of L; ::_thesis: downarrow (downarrow X) = downarrow X
A1: downarrow (downarrow X) c= downarrow X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow (downarrow X) or x in downarrow X )
assume A2: x in downarrow (downarrow X) ; ::_thesis: x in downarrow X
then reconsider x1 = x as Element of L ;
consider y being Element of L such that
A3: y >= x1 and
A4: y in downarrow X by A2, WAYBEL_0:def_15;
consider z being Element of L such that
A5: z >= y and
A6: z in X by A4, WAYBEL_0:def_15;
 z >= x1 by A3, A5, YELLOW_0:def_2;
hence  x in downarrow X by A6, WAYBEL_0:def_15; ::_thesis: verum
end;
 downarrow X c= downarrow (downarrow X) by WAYBEL_0:16;
hence  downarrow (downarrow X) = downarrow X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL23:8
for L being reflexive transitive RelStr
for X being Subset of L holds uparrow (uparrow X) = uparrow X
proof
let L be reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds uparrow (uparrow X) = uparrow X
let X be Subset of L; ::_thesis: uparrow (uparrow X) = uparrow X
A1: uparrow (uparrow X) c= uparrow X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow (uparrow X) or x in uparrow X )
assume A2: x in uparrow (uparrow X) ; ::_thesis: x in uparrow X
then reconsider x1 = x as Element of L ;
consider y being Element of L such that
A3: y <= x1 and
A4: y in uparrow X by A2, WAYBEL_0:def_16;
consider z being Element of L such that
A5: z <= y and
A6: z in X by A4, WAYBEL_0:def_16;
 z <= x1 by A3, A5, YELLOW_0:def_2;
hence  x in uparrow X by A6, WAYBEL_0:def_16; ::_thesis: verum
end;
 uparrow X c= uparrow (uparrow X) by WAYBEL_0:16;
hence  uparrow (uparrow X) = uparrow X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL23:9
for L being non empty reflexive transitive RelStr
for x being Element of L holds downarrow (downarrow x) = downarrow x
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x being Element of L holds downarrow (downarrow x) = downarrow x
let x be Element of L; ::_thesis: downarrow (downarrow x) = downarrow x
A1: downarrow (downarrow x) c= downarrow x
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in downarrow (downarrow x) or v in downarrow x )
assume A2: v in downarrow (downarrow x) ; ::_thesis: v in downarrow x
then reconsider v1 = v as Element of L ;
consider y being Element of L such that
A3: y >= v1 and
A4: y in downarrow x by A2, WAYBEL_0:def_15;
 x >= y by A4, WAYBEL_0:17;
then  x >= v1 by A3, YELLOW_0:def_2;
hence  v in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
 downarrow x c= downarrow (downarrow x) by WAYBEL_0:16;
hence  downarrow (downarrow x) = downarrow x by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL23:10
for L being non empty reflexive transitive RelStr
for x being Element of L holds uparrow (uparrow x) = uparrow x
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x being Element of L holds uparrow (uparrow x) = uparrow x
let x be Element of L; ::_thesis: uparrow (uparrow x) = uparrow x
A1: uparrow (uparrow x) c= uparrow x
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in uparrow (uparrow x) or v in uparrow x )
assume A2: v in uparrow (uparrow x) ; ::_thesis: v in uparrow x
then reconsider v1 = v as Element of L ;
consider y being Element of L such that
A3: y <= v1 and
A4: y in uparrow x by A2, WAYBEL_0:def_16;
 x <= y by A4, WAYBEL_0:18;
then  x <= v1 by A3, YELLOW_0:def_2;
hence  v in uparrow x by WAYBEL_0:18; ::_thesis: verum
end;
 uparrow x c= uparrow (uparrow x) by WAYBEL_0:16;
hence  uparrow (uparrow x) = uparrow x by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th11: :: WAYBEL23:11
for L being non empty RelStr
for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
downarrow Y c= downarrow X
proof
let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
downarrow Y c= downarrow X
let S be non empty SubRelStr of L; ::_thesis: for X being Subset of L
for Y being Subset of S st X = Y holds
downarrow Y c= downarrow X
let X be Subset of L; ::_thesis: for Y being Subset of S st X = Y holds
downarrow Y c= downarrow X
let Y be Subset of S; ::_thesis: ( X = Y implies downarrow Y c= downarrow X )
assume A1: X = Y ; ::_thesis: downarrow Y c= downarrow X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow Y or x in downarrow X )
assume A2: x in downarrow Y ; ::_thesis: x in downarrow X
then reconsider x1 = x as Element of S ;
consider y1 being Element of S such that
A3: y1 >= x1 and
A4: y1 in Y by A2, WAYBEL_0:def_15;
reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;
 y2 >= x2 by A3, YELLOW_0:59;
hence  x in downarrow X by A1, A4, WAYBEL_0:def_15; ::_thesis: verum
end;

theorem Th12: :: WAYBEL23:12
for L being non empty RelStr
for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
proof
let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
let S be non empty SubRelStr of L; ::_thesis: for X being Subset of L
for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
let X be Subset of L; ::_thesis: for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
let Y be Subset of S; ::_thesis: ( X = Y implies uparrow Y c= uparrow X )
assume A1: X = Y ; ::_thesis: uparrow Y c= uparrow X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow Y or x in uparrow X )
assume A2: x in uparrow Y ; ::_thesis: x in uparrow X
then reconsider x1 = x as Element of S ;
consider y1 being Element of S such that
A3: y1 <= x1 and
A4: y1 in Y by A2, WAYBEL_0:def_16;
reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;
 y2 <= x2 by A3, YELLOW_0:59;
hence  x in uparrow X by A1, A4, WAYBEL_0:def_16; ::_thesis: verum
end;

theorem :: WAYBEL23:13
for L being non empty RelStr
for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
downarrow y c= downarrow x
proof
let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
downarrow y c= downarrow x
let S be non empty SubRelStr of L; ::_thesis: for x being Element of L
for y being Element of S st x = y holds
downarrow y c= downarrow x
let x be Element of L; ::_thesis: for y being Element of S st x = y holds
downarrow y c= downarrow x
let y be Element of S; ::_thesis: ( x = y implies downarrow y c= downarrow x )
A1: downarrow x = downarrow {x} by WAYBEL_0:def_17;
A2: downarrow y = downarrow {y} by WAYBEL_0:def_17;
assume  x = y ; ::_thesis: downarrow y c= downarrow x
hence  downarrow y c= downarrow x by A1, A2, Th11; ::_thesis: verum
end;

theorem :: WAYBEL23:14
for L being non empty RelStr
for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
uparrow y c= uparrow x
proof
let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
uparrow y c= uparrow x
let S be non empty SubRelStr of L; ::_thesis: for x being Element of L
for y being Element of S st x = y holds
uparrow y c= uparrow x
let x be Element of L; ::_thesis: for y being Element of S st x = y holds
uparrow y c= uparrow x
let y be Element of S; ::_thesis: ( x = y implies uparrow y c= uparrow x )
A1: uparrow x = uparrow {x} by WAYBEL_0:def_18;
A2: uparrow y = uparrow {y} by WAYBEL_0:def_18;
assume  x = y ; ::_thesis: uparrow y c= uparrow x
hence  uparrow y c= uparrow x by A1, A2, Th12; ::_thesis: verum
end;

begin

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is meet-closed  means :Def1: :: WAYBEL23:def 1
 subrelstr S is meet-inheriting ;
end;

:: deftheorem Def1 defines meet-closed WAYBEL23:def_1_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is meet-closed iff subrelstr S is meet-inheriting );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is join-closed  means :Def2: :: WAYBEL23:def 2
 subrelstr S is join-inheriting ;
end;

:: deftheorem Def2 defines join-closed WAYBEL23:def_2_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is join-closed iff subrelstr S is join-inheriting );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is infs-closed  means :Def3: :: WAYBEL23:def 3
 subrelstr S is infs-inheriting ;
end;

:: deftheorem Def3 defines infs-closed WAYBEL23:def_3_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is infs-closed iff subrelstr S is infs-inheriting );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is sups-closed  means :Def4: :: WAYBEL23:def 4
 subrelstr S is sups-inheriting ;
end;

:: deftheorem Def4 defines sups-closed WAYBEL23:def_4_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is sups-closed iff subrelstr S is sups-inheriting );

registration
let L be non empty RelStr ;
cluster infs-closed  ->  meet-closed for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is infs-closed holds
b1 is meet-closed
proof
let S be Subset of L; ::_thesis: ( S is infs-closed implies S is meet-closed )
assume  S is infs-closed ; ::_thesis: S is meet-closed
then reconsider S1 = subrelstr S as infs-inheriting SubRelStr of L by Def3;
 S1 is meet-inheriting ;
hence  S is meet-closed by Def1; ::_thesis: verum
end;
cluster sups-closed  ->  join-closed for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is sups-closed holds
b1 is join-closed
proof
let S be Subset of L; ::_thesis: ( S is sups-closed implies S is join-closed )
assume  S is sups-closed ; ::_thesis: S is join-closed
then reconsider S1 = subrelstr S as sups-inheriting SubRelStr of L by Def4;
 S1 is join-inheriting ;
hence  S is join-closed by Def2; ::_thesis: verum
end;
end;

registration
let L be non empty RelStr ;
cluster non empty infs-closed sups-closed for Element of K32( the carrier of L);
existence
 ex b1 being Subset of L st
( b1 is infs-closed & b1 is sups-closed & not b1 is empty )
proof
 the carrier of L c= the carrier of L ;
then reconsider S = the carrier of L as Subset of L ;
take  S ; ::_thesis: ( S is infs-closed & S is sups-closed & not S is empty )
 the carrier of (subrelstr S) = S by YELLOW_0:def_15;
then  for X being Subset of (subrelstr S) st ex_inf_of X,L holds
"/\" (X,L) in the carrier of (subrelstr S) ;
hence  subrelstr S is infs-inheriting by YELLOW_0:def_18; :: according to WAYBEL23:def_3 ::_thesis: ( S is sups-closed & not S is empty )
 the carrier of (subrelstr S) = S by YELLOW_0:def_15;
then  for X being Subset of (subrelstr S) st ex_sup_of X,L holds
"\/" (X,L) in the carrier of (subrelstr S) ;
hence  subrelstr S is sups-inheriting by YELLOW_0:def_19; :: according to WAYBEL23:def_4 ::_thesis: not S is empty
thus  not S is empty ; ::_thesis: verum
end;
end;

theorem Th15: :: WAYBEL23:15
for L being non empty RelStr
for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
proof
let L be non empty RelStr ; ::_thesis: for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
let S be Subset of L; ::_thesis: ( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
thus  ( S is meet-closed implies for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S ) ::_thesis: ( ( for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S ) implies S is meet-closed )
proof
assume  S is meet-closed ; ::_thesis: for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S
then A1: subrelstr S is meet-inheriting by Def1;
let x, y be Element of L; ::_thesis: ( x in S & y in S & ex_inf_of {x,y},L implies inf {x,y} in S )
assume that
A2: x in S and
A3: y in S and
A4: ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in S
 the carrier of (subrelstr S) = S by YELLOW_0:def_15;
hence  inf {x,y} in S by A1, A2, A3, A4, YELLOW_0:def_16; ::_thesis: verum
end;
assume A5: for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S ; ::_thesis: S is meet-closed
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(subrelstr_S)_&_y_in_the_carrier_of_(subrelstr_S)_&_ex_inf_of_{x,y},L_holds_
inf_{x,y}_in_the_carrier_of_(subrelstr_S)
let x, y be Element of L; ::_thesis: ( x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (subrelstr S) )
assume that
A6: x in the carrier of (subrelstr S) and
A7: y in the carrier of (subrelstr S) and
A8: ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (subrelstr S)
 the carrier of (subrelstr S) = S by YELLOW_0:def_15;
hence  inf {x,y} in the carrier of (subrelstr S) by A5, A6, A7, A8; ::_thesis: verum
end;
then  subrelstr S is meet-inheriting by YELLOW_0:def_16;
hence  S is meet-closed by Def1; ::_thesis: verum
end;

theorem Th16: :: WAYBEL23:16
for L being non empty RelStr
for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )
proof
let L be non empty RelStr ; ::_thesis: for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )
let S be Subset of L; ::_thesis: ( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )
thus  ( S is join-closed implies for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ) ::_thesis: ( ( for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ) implies S is join-closed )
proof
assume  S is join-closed ; ::_thesis: for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S
then A1: subrelstr S is join-inheriting by Def2;
let x, y be Element of L; ::_thesis: ( x in S & y in S & ex_sup_of {x,y},L implies sup {x,y} in S )
assume that
A2: x in S and
A3: y in S and
A4: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in S
 the carrier of (subrelstr S) = S by YELLOW_0:def_15;
hence  sup {x,y} in S by A1, A2, A3, A4, YELLOW_0:def_17; ::_thesis: verum
end;
assume A5: for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ; ::_thesis: S is join-closed
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(subrelstr_S)_&_y_in_the_carrier_of_(subrelstr_S)_&_ex_sup_of_{x,y},L_holds_
sup_{x,y}_in_the_carrier_of_(subrelstr_S)
let x, y be Element of L; ::_thesis: ( x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (subrelstr S) )
assume that
A6: x in the carrier of (subrelstr S) and
A7: y in the carrier of (subrelstr S) and
A8: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (subrelstr S)
 the carrier of (subrelstr S) = S by YELLOW_0:def_15;
hence  sup {x,y} in the carrier of (subrelstr S) by A5, A6, A7, A8; ::_thesis: verum
end;
then  subrelstr S is join-inheriting by YELLOW_0:def_17;
hence  S is join-closed by Def2; ::_thesis: verum
end;

theorem :: WAYBEL23:17
for L being antisymmetric with_infima RelStr
for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S holds
inf {x,y} in S )
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S holds
inf {x,y} in S )
let S be Subset of L; ::_thesis: ( S is meet-closed iff for x, y being Element of L st x in S & y in S holds
inf {x,y} in S )
thus  ( S is meet-closed implies for x, y being Element of L st x in S & y in S holds
inf {x,y} in S ) ::_thesis: ( ( for x, y being Element of L st x in S & y in S holds
inf {x,y} in S ) implies S is meet-closed )
proof
assume A1: S is meet-closed ; ::_thesis: for x, y being Element of L st x in S & y in S holds
inf {x,y} in S
let x, y be Element of L; ::_thesis: ( x in S & y in S implies inf {x,y} in S )
assume that
A2: x in S and
A3: y in S ; ::_thesis: inf {x,y} in S
 ex_inf_of {x,y},L by YELLOW_0:21;
hence  inf {x,y} in S by A1, A2, A3, Th15; ::_thesis: verum
end;
assume  for x, y being Element of L st x in S & y in S holds
inf {x,y} in S ; ::_thesis: S is meet-closed
then  for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S ;
hence  S is meet-closed by Th15; ::_thesis: verum
end;

theorem Th18: :: WAYBEL23:18
for L being antisymmetric with_suprema RelStr
for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S holds
sup {x,y} in S )
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S holds
sup {x,y} in S )
let S be Subset of L; ::_thesis: ( S is join-closed iff for x, y being Element of L st x in S & y in S holds
sup {x,y} in S )
thus  ( S is join-closed implies for x, y being Element of L st x in S & y in S holds
sup {x,y} in S ) ::_thesis: ( ( for x, y being Element of L st x in S & y in S holds
sup {x,y} in S ) implies S is join-closed )
proof
assume A1: S is join-closed ; ::_thesis: for x, y being Element of L st x in S & y in S holds
sup {x,y} in S
let x, y be Element of L; ::_thesis: ( x in S & y in S implies sup {x,y} in S )
assume that
A2: x in S and
A3: y in S ; ::_thesis: sup {x,y} in S
 ex_sup_of {x,y},L by YELLOW_0:20;
hence  sup {x,y} in S by A1, A2, A3, Th16; ::_thesis: verum
end;
assume  for x, y being Element of L st x in S & y in S holds
sup {x,y} in S ; ::_thesis: S is join-closed
then  for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ;
hence  S is join-closed by Th16; ::_thesis: verum
end;

theorem :: WAYBEL23:19
for L being non empty RelStr
for S being Subset of L holds
( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
proof
let L be non empty RelStr ; ::_thesis: for S being Subset of L holds
( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
let S be Subset of L; ::_thesis: ( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
thus  ( S is infs-closed implies for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S ) ::_thesis: ( ( for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S ) implies S is infs-closed )
proof
assume  S is infs-closed ; ::_thesis: for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S
then A1: subrelstr S is infs-inheriting by Def3;
let X be Subset of S; ::_thesis: ( ex_inf_of X,L implies "/\" (X,L) in S )
assume A2: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in S
 X is Subset of (subrelstr S) by YELLOW_0:def_15;
then  "/\" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def_18;
hence  "/\" (X,L) in S by YELLOW_0:def_15; ::_thesis: verum
end;
assume A3: for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S ; ::_thesis: S is infs-closed
now__::_thesis:_for_X_being_Subset_of_(subrelstr_S)_st_ex_inf_of_X,L_holds_
"/\"_(X,L)_in_the_carrier_of_(subrelstr_S)
let X be Subset of (subrelstr S); ::_thesis: ( ex_inf_of X,L implies "/\" (X,L) in the carrier of (subrelstr S) )
assume A4: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr S)
 X is Subset of S by YELLOW_0:def_15;
then  "/\" (X,L) in S by A3, A4;
hence  "/\" (X,L) in the carrier of (subrelstr S) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr S is infs-inheriting by YELLOW_0:def_18;
hence  S is infs-closed by Def3; ::_thesis: verum
end;

theorem :: WAYBEL23:20
for L being non empty RelStr
for S being Subset of L holds
( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S )
proof
let L be non empty RelStr ; ::_thesis: for S being Subset of L holds
( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S )
let S be Subset of L; ::_thesis: ( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S )
thus  ( S is sups-closed implies for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S ) ::_thesis: ( ( for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S ) implies S is sups-closed )
proof
assume  S is sups-closed ; ::_thesis: for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S
then A1: subrelstr S is sups-inheriting by Def4;
let X be Subset of S; ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) in S )
assume A2: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in S
 X is Subset of (subrelstr S) by YELLOW_0:def_15;
then  "\/" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def_19;
hence  "\/" (X,L) in S by YELLOW_0:def_15; ::_thesis: verum
end;
assume A3: for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S ; ::_thesis: S is sups-closed
now__::_thesis:_for_X_being_Subset_of_(subrelstr_S)_st_ex_sup_of_X,L_holds_
"\/"_(X,L)_in_the_carrier_of_(subrelstr_S)
let X be Subset of (subrelstr S); ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) in the carrier of (subrelstr S) )
assume A4: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr S)
 X is Subset of S by YELLOW_0:def_15;
then  "\/" (X,L) in S by A3, A4;
hence  "\/" (X,L) in the carrier of (subrelstr S) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr S is sups-inheriting by YELLOW_0:def_19;
hence  S is sups-closed by Def4; ::_thesis: verum
end;

theorem Th21: :: WAYBEL23:21
for L being non empty transitive RelStr
for S being non empty infs-closed Subset of L
for X being Subset of S st ex_inf_of X,L holds
( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty infs-closed Subset of L
for X being Subset of S st ex_inf_of X,L holds
( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
let S be non empty infs-closed Subset of L; ::_thesis: for X being Subset of S st ex_inf_of X,L holds
( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
let X be Subset of S; ::_thesis: ( ex_inf_of X,L implies ( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) ) )
A1: X is Subset of (subrelstr S) by YELLOW_0:def_15;
assume A2: ex_inf_of X,L ; ::_thesis: ( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
 subrelstr S is non empty full infs-inheriting SubRelStr of L by Def3;
then  "/\" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def_18;
hence  ( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) ) by A1, A2, YELLOW_0:63; ::_thesis: verum
end;

theorem Th22: :: WAYBEL23:22
for L being non empty transitive RelStr
for S being non empty sups-closed Subset of L
for X being Subset of S st ex_sup_of X,L holds
( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty sups-closed Subset of L
for X being Subset of S st ex_sup_of X,L holds
( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )
let S be non empty sups-closed Subset of L; ::_thesis: for X being Subset of S st ex_sup_of X,L holds
( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )
let X be Subset of S; ::_thesis: ( ex_sup_of X,L implies ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) ) )
A1: X is Subset of (subrelstr S) by YELLOW_0:def_15;
assume A2: ex_sup_of X,L ; ::_thesis: ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )
 subrelstr S is non empty full sups-inheriting SubRelStr of L by Def4;
then  "\/" (X,L) in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def_19;
hence  ( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) ) by A1, A2, YELLOW_0:64; ::_thesis: verum
end;

theorem :: WAYBEL23:23
for L being non empty transitive RelStr
for S being non empty meet-closed Subset of L
for x, y being Element of S st ex_inf_of {x,y},L holds
( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty meet-closed Subset of L
for x, y being Element of S st ex_inf_of {x,y},L holds
( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )
let S be non empty meet-closed Subset of L; ::_thesis: for x, y being Element of S st ex_inf_of {x,y},L holds
( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )
let x, y be Element of S; ::_thesis: ( ex_inf_of {x,y},L implies ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) ) )
A1: x is Element of (subrelstr S) by YELLOW_0:def_15;
A2: y is Element of (subrelstr S) by YELLOW_0:def_15;
assume A3: ex_inf_of {x,y},L ; ::_thesis: ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )
 subrelstr S is non empty full meet-inheriting SubRelStr of L by Def1;
then  "/\" ({x,y},L) in the carrier of (subrelstr S) by A1, A2, A3, YELLOW_0:def_16;
hence  ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) ) by A1, A2, A3, YELLOW_0:65; ::_thesis: verum
end;

theorem :: WAYBEL23:24
for L being non empty transitive RelStr
for S being non empty join-closed Subset of L
for x, y being Element of S st ex_sup_of {x,y},L holds
( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty join-closed Subset of L
for x, y being Element of S st ex_sup_of {x,y},L holds
( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )
let S be non empty join-closed Subset of L; ::_thesis: for x, y being Element of S st ex_sup_of {x,y},L holds
( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )
let x, y be Element of S; ::_thesis: ( ex_sup_of {x,y},L implies ( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) ) )
A1: x is Element of (subrelstr S) by YELLOW_0:def_15;
A2: y is Element of (subrelstr S) by YELLOW_0:def_15;
assume A3: ex_sup_of {x,y},L ; ::_thesis: ( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )
 subrelstr S is non empty full join-inheriting SubRelStr of L by Def2;
then  "\/" ({x,y},L) in the carrier of (subrelstr S) by A1, A2, A3, YELLOW_0:def_17;
hence  ( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) ) by A1, A2, A3, YELLOW_0:66; ::_thesis: verum
end;

theorem Th25: :: WAYBEL23:25
for L being transitive antisymmetric with_infima RelStr
for S being non empty meet-closed Subset of L holds subrelstr S is with_infima
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for S being non empty meet-closed Subset of L holds subrelstr S is with_infima
let S be non empty meet-closed Subset of L; ::_thesis: subrelstr S is with_infima
 subrelstr S is non empty full meet-inheriting SubRelStr of L by Def1;
hence  subrelstr S is with_infima ; ::_thesis: verum
end;

theorem Th26: :: WAYBEL23:26
for L being transitive antisymmetric with_suprema RelStr
for S being non empty join-closed Subset of L holds subrelstr S is with_suprema
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for S being non empty join-closed Subset of L holds subrelstr S is with_suprema
let S be non empty join-closed Subset of L; ::_thesis: subrelstr S is with_suprema
 subrelstr S is non empty full join-inheriting SubRelStr of L by Def2;
hence  subrelstr S is with_suprema ; ::_thesis: verum
end;

registration
let L be transitive antisymmetric with_infima RelStr ;
let S be non empty meet-closed Subset of L;
cluster subrelstr S ->  with_infima ;
coherence
 subrelstr S is with_infima by Th25;
end;

registration
let L be transitive antisymmetric with_suprema RelStr ;
let S be non empty join-closed Subset of L;
cluster subrelstr S ->  with_suprema ;
coherence
 subrelstr S is with_suprema by Th26;
end;

theorem :: WAYBEL23:27
for L being non empty transitive antisymmetric complete RelStr
for S being non empty infs-closed Subset of L
for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)
proof
let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for S being non empty infs-closed Subset of L
for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)
let S be non empty infs-closed Subset of L; ::_thesis: for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)
let X be Subset of S; ::_thesis: "/\" (X,(subrelstr S)) = "/\" (X,L)
 ex_inf_of X,L by YELLOW_0:17;
hence  "/\" (X,(subrelstr S)) = "/\" (X,L) by Th21; ::_thesis: verum
end;

theorem :: WAYBEL23:28
for L being non empty transitive antisymmetric complete RelStr
for S being non empty sups-closed Subset of L
for X being Subset of S holds "\/" (X,(subrelstr S)) = "\/" (X,L)
proof
let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for S being non empty sups-closed Subset of L
for X being Subset of S holds "\/" (X,(subrelstr S)) = "\/" (X,L)
let S be non empty sups-closed Subset of L; ::_thesis: for X being Subset of S holds "\/" (X,(subrelstr S)) = "\/" (X,L)
let X be Subset of S; ::_thesis: "\/" (X,(subrelstr S)) = "\/" (X,L)
 ex_sup_of X,L by YELLOW_0:17;
hence  "\/" (X,(subrelstr S)) = "\/" (X,L) by Th22; ::_thesis: verum
end;

theorem Th29: :: WAYBEL23:29
for L being Semilattice
for S being meet-closed Subset of L holds S is filtered
proof
let L be Semilattice; ::_thesis: for S being meet-closed Subset of L holds S is filtered
let S be meet-closed Subset of L; ::_thesis: S is filtered
 subrelstr S is meet-inheriting by Def1;
hence  S is filtered by YELLOW12:26; ::_thesis: verum
end;

theorem Th30: :: WAYBEL23:30
for L being sup-Semilattice
for S being join-closed Subset of L holds S is directed
proof
let L be sup-Semilattice; ::_thesis: for S being join-closed Subset of L holds S is directed
let S be join-closed Subset of L; ::_thesis: S is directed
 subrelstr S is join-inheriting by Def2;
hence  S is directed by YELLOW12:27; ::_thesis: verum
end;

registration
let L be Semilattice;
cluster meet-closed  ->  filtered for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is meet-closed holds
b1 is filtered by Th29;
end;

registration
let L be sup-Semilattice;
cluster join-closed  ->  directed for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is join-closed holds
b1 is directed by Th30;
end;

theorem :: WAYBEL23:31
for L being Semilattice
for S being non empty upper Subset of L holds
( S is Filter of L iff S is meet-closed )
proof
let L be Semilattice; ::_thesis: for S being non empty upper Subset of L holds
( S is Filter of L iff S is meet-closed )
let S be non empty upper Subset of L; ::_thesis: ( S is Filter of L iff S is meet-closed )
 ( S is Filter of L iff subrelstr S is meet-inheriting ) by WAYBEL_0:63;
hence  ( S is Filter of L iff S is meet-closed ) by Def1; ::_thesis: verum
end;

theorem :: WAYBEL23:32
for L being sup-Semilattice
for S being non empty lower Subset of L holds
( S is Ideal of L iff S is join-closed )
proof
let L be sup-Semilattice; ::_thesis: for S being non empty lower Subset of L holds
( S is Ideal of L iff S is join-closed )
let S be non empty lower Subset of L; ::_thesis: ( S is Ideal of L iff S is join-closed )
 ( S is Ideal of L iff subrelstr S is join-inheriting ) by WAYBEL_0:64;
hence  ( S is Ideal of L iff S is join-closed ) by Def2; ::_thesis: verum
end;

theorem Th33: :: WAYBEL23:33
for L being non empty RelStr
for S1, S2 being join-closed Subset of L holds S1 /\ S2 is join-closed
proof
let L be non empty RelStr ; ::_thesis: for S1, S2 being join-closed Subset of L holds S1 /\ S2 is join-closed
let S1, S2 be join-closed Subset of L; ::_thesis: S1 /\ S2 is join-closed
A1: subrelstr S2 is join-inheriting by Def2;
A2: subrelstr S1 is join-inheriting by Def2;
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(subrelstr_(S1_/\_S2))_&_y_in_the_carrier_of_(subrelstr_(S1_/\_S2))_&_ex_sup_of_{x,y},L_holds_
sup_{x,y}_in_the_carrier_of_(subrelstr_(S1_/\_S2))
let x, y be Element of L; ::_thesis: ( x in the carrier of (subrelstr (S1 /\ S2)) & y in the carrier of (subrelstr (S1 /\ S2)) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (subrelstr (S1 /\ S2)) )
assume that
A3: x in the carrier of (subrelstr (S1 /\ S2)) and
A4: y in the carrier of (subrelstr (S1 /\ S2)) and
A5: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (subrelstr (S1 /\ S2))
A6: y in S1 /\ S2 by A4, YELLOW_0:def_15;
then  y in S2 by XBOOLE_0:def_4;
then A7: y in the carrier of (subrelstr S2) by YELLOW_0:def_15;
A8: x in S1 /\ S2 by A3, YELLOW_0:def_15;
then  x in S2 by XBOOLE_0:def_4;
then  x in the carrier of (subrelstr S2) by YELLOW_0:def_15;
then  sup {x,y} in the carrier of (subrelstr S2) by A1, A5, A7, YELLOW_0:def_17;
then A9: sup {x,y} in S2 by YELLOW_0:def_15;
 y in S1 by A6, XBOOLE_0:def_4;
then A10: y in the carrier of (subrelstr S1) by YELLOW_0:def_15;
 x in S1 by A8, XBOOLE_0:def_4;
then  x in the carrier of (subrelstr S1) by YELLOW_0:def_15;
then  sup {x,y} in the carrier of (subrelstr S1) by A2, A5, A10, YELLOW_0:def_17;
then  sup {x,y} in S1 by YELLOW_0:def_15;
then  sup {x,y} in S1 /\ S2 by A9, XBOOLE_0:def_4;
hence  sup {x,y} in the carrier of (subrelstr (S1 /\ S2)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (S1 /\ S2) is join-inheriting by YELLOW_0:def_17;
hence  S1 /\ S2 is join-closed by Def2; ::_thesis: verum
end;

theorem :: WAYBEL23:34
for L being non empty RelStr
for S1, S2 being meet-closed Subset of L holds S1 /\ S2 is meet-closed
proof
let L be non empty RelStr ; ::_thesis: for S1, S2 being meet-closed Subset of L holds S1 /\ S2 is meet-closed
let S1, S2 be meet-closed Subset of L; ::_thesis: S1 /\ S2 is meet-closed
A1: subrelstr S2 is meet-inheriting by Def1;
A2: subrelstr S1 is meet-inheriting by Def1;
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(subrelstr_(S1_/\_S2))_&_y_in_the_carrier_of_(subrelstr_(S1_/\_S2))_&_ex_inf_of_{x,y},L_holds_
inf_{x,y}_in_the_carrier_of_(subrelstr_(S1_/\_S2))
let x, y be Element of L; ::_thesis: ( x in the carrier of (subrelstr (S1 /\ S2)) & y in the carrier of (subrelstr (S1 /\ S2)) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (subrelstr (S1 /\ S2)) )
assume that
A3: x in the carrier of (subrelstr (S1 /\ S2)) and
A4: y in the carrier of (subrelstr (S1 /\ S2)) and
A5: ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (subrelstr (S1 /\ S2))
A6: y in S1 /\ S2 by A4, YELLOW_0:def_15;
then  y in S2 by XBOOLE_0:def_4;
then A7: y in the carrier of (subrelstr S2) by YELLOW_0:def_15;
A8: x in S1 /\ S2 by A3, YELLOW_0:def_15;
then  x in S2 by XBOOLE_0:def_4;
then  x in the carrier of (subrelstr S2) by YELLOW_0:def_15;
then  inf {x,y} in the carrier of (subrelstr S2) by A1, A5, A7, YELLOW_0:def_16;
then A9: inf {x,y} in S2 by YELLOW_0:def_15;
 y in S1 by A6, XBOOLE_0:def_4;
then A10: y in the carrier of (subrelstr S1) by YELLOW_0:def_15;
 x in S1 by A8, XBOOLE_0:def_4;
then  x in the carrier of (subrelstr S1) by YELLOW_0:def_15;
then  inf {x,y} in the carrier of (subrelstr S1) by A2, A5, A10, YELLOW_0:def_16;
then  inf {x,y} in S1 by YELLOW_0:def_15;
then  inf {x,y} in S1 /\ S2 by A9, XBOOLE_0:def_4;
hence  inf {x,y} in the carrier of (subrelstr (S1 /\ S2)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (S1 /\ S2) is meet-inheriting by YELLOW_0:def_16;
hence  S1 /\ S2 is meet-closed by Def1; ::_thesis: verum
end;

theorem Th35: :: WAYBEL23:35
for L being sup-Semilattice
for x being Element of L holds downarrow x is join-closed
proof
let L be sup-Semilattice; ::_thesis: for x being Element of L holds downarrow x is join-closed
let x be Element of L; ::_thesis: downarrow x is join-closed
reconsider x1 = x as Element of L ;
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(downarrow_x))_&_z_in_the_carrier_of_(subrelstr_(downarrow_x))_&_ex_sup_of_{y,z},L_holds_
sup_{y,z}_in_the_carrier_of_(subrelstr_(downarrow_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (downarrow x)) & z in the carrier of (subrelstr (downarrow x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (downarrow x)) )
assume that
A1: y in the carrier of (subrelstr (downarrow x)) and
A2: z in the carrier of (subrelstr (downarrow x)) and
 ex_sup_of {y,z},L ; ::_thesis: sup {y,z} in the carrier of (subrelstr (downarrow x))
 z in downarrow x by A2, YELLOW_0:def_15;
then A3: z <= x1 by WAYBEL_0:17;
 y in downarrow x by A1, YELLOW_0:def_15;
then  y <= x1 by WAYBEL_0:17;
then  y "\/" z <= x1 by A3, YELLOW_5:9;
then  y "\/" z in downarrow x by WAYBEL_0:17;
then  sup {y,z} in downarrow x by YELLOW_0:41;
hence  sup {y,z} in the carrier of (subrelstr (downarrow x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (downarrow x) is join-inheriting by YELLOW_0:def_17;
hence  downarrow x is join-closed by Def2; ::_thesis: verum
end;

theorem Th36: :: WAYBEL23:36
for L being Semilattice
for x being Element of L holds downarrow x is meet-closed
proof
let L be Semilattice; ::_thesis: for x being Element of L holds downarrow x is meet-closed
let x be Element of L; ::_thesis: downarrow x is meet-closed
reconsider x1 = x as Element of L ;
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(downarrow_x))_&_z_in_the_carrier_of_(subrelstr_(downarrow_x))_&_ex_inf_of_{y,z},L_holds_
inf_{y,z}_in_the_carrier_of_(subrelstr_(downarrow_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (downarrow x)) & z in the carrier of (subrelstr (downarrow x)) & ex_inf_of {y,z},L implies inf {y,z} in the carrier of (subrelstr (downarrow x)) )
assume that
A1: y in the carrier of (subrelstr (downarrow x)) and
 z in the carrier of (subrelstr (downarrow x)) and
 ex_inf_of {y,z},L ; ::_thesis: inf {y,z} in the carrier of (subrelstr (downarrow x))
 y in downarrow x by A1, YELLOW_0:def_15;
then A2: y <= x1 by WAYBEL_0:17;
 y "/\" z <= y by YELLOW_0:23;
then  y "/\" z <= x1 by A2, YELLOW_0:def_2;
then  y "/\" z in downarrow x by WAYBEL_0:17;
then  inf {y,z} in downarrow x by YELLOW_0:40;
hence  inf {y,z} in the carrier of (subrelstr (downarrow x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (downarrow x) is meet-inheriting by YELLOW_0:def_16;
hence  downarrow x is meet-closed by Def1; ::_thesis: verum
end;

theorem Th37: :: WAYBEL23:37
for L being sup-Semilattice
for x being Element of L holds uparrow x is join-closed
proof
let L be sup-Semilattice; ::_thesis: for x being Element of L holds uparrow x is join-closed
let x be Element of L; ::_thesis: uparrow x is join-closed
reconsider x1 = x as Element of L ;
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(uparrow_x))_&_z_in_the_carrier_of_(subrelstr_(uparrow_x))_&_ex_sup_of_{y,z},L_holds_
sup_{y,z}_in_the_carrier_of_(subrelstr_(uparrow_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (uparrow x)) & z in the carrier of (subrelstr (uparrow x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (uparrow x)) )
assume that
A1: y in the carrier of (subrelstr (uparrow x)) and
 z in the carrier of (subrelstr (uparrow x)) and
 ex_sup_of {y,z},L ; ::_thesis: sup {y,z} in the carrier of (subrelstr (uparrow x))
 y in uparrow x by A1, YELLOW_0:def_15;
then A2: y >= x1 by WAYBEL_0:18;
 y "\/" z >= y by YELLOW_0:22;
then  y "\/" z >= x1 by A2, YELLOW_0:def_2;
then  y "\/" z in uparrow x by WAYBEL_0:18;
then  sup {y,z} in uparrow x by YELLOW_0:41;
hence  sup {y,z} in the carrier of (subrelstr (uparrow x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (uparrow x) is join-inheriting by YELLOW_0:def_17;
hence  uparrow x is join-closed by Def2; ::_thesis: verum
end;

theorem Th38: :: WAYBEL23:38
for L being Semilattice
for x being Element of L holds uparrow x is meet-closed
proof
let L be Semilattice; ::_thesis: for x being Element of L holds uparrow x is meet-closed
let x be Element of L; ::_thesis: uparrow x is meet-closed
reconsider x1 = x as Element of L ;
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(uparrow_x))_&_z_in_the_carrier_of_(subrelstr_(uparrow_x))_&_ex_inf_of_{y,z},L_holds_
inf_{y,z}_in_the_carrier_of_(subrelstr_(uparrow_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (uparrow x)) & z in the carrier of (subrelstr (uparrow x)) & ex_inf_of {y,z},L implies inf {y,z} in the carrier of (subrelstr (uparrow x)) )
assume that
A1: y in the carrier of (subrelstr (uparrow x)) and
A2: z in the carrier of (subrelstr (uparrow x)) and
 ex_inf_of {y,z},L ; ::_thesis: inf {y,z} in the carrier of (subrelstr (uparrow x))
 z in uparrow x by A2, YELLOW_0:def_15;
then A3: z >= x1 by WAYBEL_0:18;
 y in uparrow x by A1, YELLOW_0:def_15;
then  y >= x1 by WAYBEL_0:18;
then  y "/\" z >= x1 "/\" x1 by A3, YELLOW_3:2;
then  y "/\" z >= x1 by YELLOW_5:2;
then  y "/\" z in uparrow x by WAYBEL_0:18;
then  inf {y,z} in uparrow x by YELLOW_0:40;
hence  inf {y,z} in the carrier of (subrelstr (uparrow x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (uparrow x) is meet-inheriting by YELLOW_0:def_16;
hence  uparrow x is meet-closed by Def1; ::_thesis: verum
end;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster downarrow x ->  join-closed ;
coherence
 downarrow x is join-closed by Th35;
cluster uparrow x ->  join-closed ;
coherence
 uparrow x is join-closed by Th37;
end;

registration
let L be Semilattice;
let x be Element of L;
cluster downarrow x ->  meet-closed ;
coherence
 downarrow x is meet-closed by Th36;
cluster uparrow x ->  meet-closed ;
coherence
 uparrow x is meet-closed by Th38;
end;

theorem Th39: :: WAYBEL23:39
for L being sup-Semilattice
for x being Element of L holds waybelow x is join-closed
proof
let L be sup-Semilattice; ::_thesis: for x being Element of L holds waybelow x is join-closed
let x be Element of L; ::_thesis: waybelow x is join-closed
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(waybelow_x))_&_z_in_the_carrier_of_(subrelstr_(waybelow_x))_&_ex_sup_of_{y,z},L_holds_
sup_{y,z}_in_the_carrier_of_(subrelstr_(waybelow_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (waybelow x)) & z in the carrier of (subrelstr (waybelow x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (waybelow x)) )
assume that
A1: y in the carrier of (subrelstr (waybelow x)) and
A2: z in the carrier of (subrelstr (waybelow x)) and
 ex_sup_of {y,z},L ; ::_thesis: sup {y,z} in the carrier of (subrelstr (waybelow x))
 z in waybelow x by A2, YELLOW_0:def_15;
then A3: z << x by WAYBEL_3:7;
 y in waybelow x by A1, YELLOW_0:def_15;
then  y << x by WAYBEL_3:7;
then  y "\/" z << x by A3, WAYBEL_3:3;
then  y "\/" z in waybelow x by WAYBEL_3:7;
then  sup {y,z} in waybelow x by YELLOW_0:41;
hence  sup {y,z} in the carrier of (subrelstr (waybelow x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (waybelow x) is join-inheriting by YELLOW_0:def_17;
hence  waybelow x is join-closed by Def2; ::_thesis: verum
end;

theorem Th40: :: WAYBEL23:40
for L being Semilattice
for x being Element of L holds waybelow x is meet-closed
proof
let L be Semilattice; ::_thesis: for x being Element of L holds waybelow x is meet-closed
let x be Element of L; ::_thesis: waybelow x is meet-closed
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(waybelow_x))_&_z_in_the_carrier_of_(subrelstr_(waybelow_x))_&_ex_inf_of_{y,z},L_holds_
inf_{y,z}_in_the_carrier_of_(subrelstr_(waybelow_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (waybelow x)) & z in the carrier of (subrelstr (waybelow x)) & ex_inf_of {y,z},L implies inf {y,z} in the carrier of (subrelstr (waybelow x)) )
assume that
A1: y in the carrier of (subrelstr (waybelow x)) and
 z in the carrier of (subrelstr (waybelow x)) and
 ex_inf_of {y,z},L ; ::_thesis: inf {y,z} in the carrier of (subrelstr (waybelow x))
 y in waybelow x by A1, YELLOW_0:def_15;
then A2: y << x by WAYBEL_3:7;
 y "/\" z <= y by YELLOW_0:23;
then  y "/\" z << x by A2, WAYBEL_3:2;
then  y "/\" z in waybelow x by WAYBEL_3:7;
then  inf {y,z} in waybelow x by YELLOW_0:40;
hence  inf {y,z} in the carrier of (subrelstr (waybelow x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (waybelow x) is meet-inheriting by YELLOW_0:def_16;
hence  waybelow x is meet-closed by Def1; ::_thesis: verum
end;

theorem Th41: :: WAYBEL23:41
for L being sup-Semilattice
for x being Element of L holds wayabove x is join-closed
proof
let L be sup-Semilattice; ::_thesis: for x being Element of L holds wayabove x is join-closed
let x be Element of L; ::_thesis: wayabove x is join-closed
now__::_thesis:_for_y,_z_being_Element_of_L_st_y_in_the_carrier_of_(subrelstr_(wayabove_x))_&_z_in_the_carrier_of_(subrelstr_(wayabove_x))_&_ex_sup_of_{y,z},L_holds_
sup_{y,z}_in_the_carrier_of_(subrelstr_(wayabove_x))
let y, z be Element of L; ::_thesis: ( y in the carrier of (subrelstr (wayabove x)) & z in the carrier of (subrelstr (wayabove x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (wayabove x)) )
assume that
A1: y in the carrier of (subrelstr (wayabove x)) and
 z in the carrier of (subrelstr (wayabove x)) and
 ex_sup_of {y,z},L ; ::_thesis: sup {y,z} in the carrier of (subrelstr (wayabove x))
 y in wayabove x by A1, YELLOW_0:def_15;
then A2: y >> x by WAYBEL_3:8;
 y "\/" z >= y by YELLOW_0:22;
then  y "\/" z >> x by A2, WAYBEL_3:2;
then  y "\/" z in wayabove x by WAYBEL_3:8;
then  sup {y,z} in wayabove x by YELLOW_0:41;
hence  sup {y,z} in the carrier of (subrelstr (wayabove x)) by YELLOW_0:def_15; ::_thesis: verum
end;
then  subrelstr (wayabove x) is join-inheriting by YELLOW_0:def_17;
hence  wayabove x is join-closed by Def2; ::_thesis: verum
end;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x ->  join-closed ;
coherence
 waybelow x is join-closed by Th39;
cluster wayabove x ->  join-closed ;
coherence
 wayabove x is join-closed by Th41;
end;

registration
let L be Semilattice;
let x be Element of L;
cluster waybelow x ->  meet-closed ;
coherence
 waybelow x is meet-closed by Th40;
end;

begin

definition
let T be TopStruct ;
func weight T ->  Cardinal equals :: WAYBEL23:def 5
 meet  {  (card B) where B is Basis of T : verum  }  ;
coherence
 meet  {  (card B) where B is Basis of T : verum  }  is Cardinal
proof
set X =  {  (card B1) where B1 is Basis of T : verum  }  ;
defpred S1[ Ordinal] means $1 in  {  (card B) where B is Basis of T : verum  }  ;
A1: ex A being Ordinal st S1[A]
proof
take  card the topology of T ; ::_thesis: S1[ card the topology of T]
 the topology of T is Basis of T by CANTOR_1:2;
hence  S1[ card the topology of T] ; ::_thesis: verum
end;
consider A being Ordinal such that
A2: S1[A] and
A3: for C being Ordinal st S1[C] holds
A c= C from ORDINAL1:sch_1(A1);
 ex B being Basis of T st A = card B by A2;
then reconsider A = A as Cardinal ;
A4: now__::_thesis:_for_x_being_set_holds_
(_(_(_for_y_being_set_st_y_in__{__(card_B1)_where_B1_is_Basis_of_T_:_verum__}__holds_
x_in_y_)_implies_x_in_A_)_&_(_x_in_A_implies_for_y_being_set_st_y_in__{__(card_B1)_where_B1_is_Basis_of_T_:_verum__}__holds_
x_in_y_)_)
let x be set ; ::_thesis: ( ( ( for y being set st y in  {  (card B1) where B1 is Basis of T : verum  }  holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in  {  (card B1) where B1 is Basis of T : verum  }  holds
x in y ) )
thus  ( ( for y being set st y in  {  (card B1) where B1 is Basis of T : verum  }  holds
x in y ) implies x in A ) by A2; ::_thesis: ( x in A implies for y being set st y in  {  (card B1) where B1 is Basis of T : verum  }  holds
x in y )
assume A5: x in A ; ::_thesis: for y being set st y in  {  (card B1) where B1 is Basis of T : verum  }  holds
x in y
let y be set ; ::_thesis: ( y in  {  (card B1) where B1 is Basis of T : verum  }  implies x in y )
assume A6: y in  {  (card B1) where B1 is Basis of T : verum  }  ; ::_thesis: x in y
then  ex B1 being Basis of T st y = card B1 ;
then reconsider y1 = y as Cardinal ;
 A c= y1 by A3, A6;
hence  x in y by A5; ::_thesis: verum
end;
 the topology of T is Basis of T by CANTOR_1:2;
then  card the topology of T in  {  (card B1) where B1 is Basis of T : verum  }  ;
hence  meet  {  (card B) where B is Basis of T : verum  }  is Cardinal by A4, SETFAM_1:def_1; ::_thesis: verum
end;
end;

:: deftheorem  defines weight WAYBEL23:def_5_:_
 for T being TopStruct holds weight T = meet  {  (card B) where B is Basis of T : verum  }  ;

definition
let T be TopStruct ;
attrT is second-countable  means :: WAYBEL23:def 6
 weight T c= omega ;
end;

:: deftheorem  defines second-countable WAYBEL23:def_6_:_
 for T being TopStruct holds
( T is second-countable iff weight T c= omega );

definition
let L be continuous sup-Semilattice;
mode CLbasis of L ->  Subset of L means :Def7: :: WAYBEL23:def 7
( it is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ it) ) );
existence
 ex b1 being Subset of L st
( b1 is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b1) ) )
proof
take S = [#] L; ::_thesis: ( S is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ S) ) )
 subrelstr S is join-inheriting by WAYBEL_0:64;
hence  S is join-closed by Def2; ::_thesis: for x being Element of L holds x = sup ((waybelow x) /\ S)
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ S)
thus x = sup (waybelow x) by WAYBEL_3:def_5
.= sup ((waybelow x) /\ S) by XBOOLE_1:28 ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines CLbasis WAYBEL23:def_7_:_
 for L being continuous sup-Semilattice
for b2 being Subset of L holds
( b2 is CLbasis of L iff ( b2 is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b2) ) ) );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is with_bottom  means :Def8: :: WAYBEL23:def 8
 Bottom L in S;
end;

:: deftheorem Def8 defines with_bottom WAYBEL23:def_8_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is with_bottom iff Bottom L in S );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is with_top  means :Def9: :: WAYBEL23:def 9
 Top L in S;
end;

:: deftheorem Def9 defines with_top WAYBEL23:def_9_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is with_top iff Top L in S );

registration
let L be non empty RelStr ;
cluster with_bottom  ->  non empty for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is with_bottom holds
not b1 is empty by Def8;
end;

registration
let L be non empty RelStr ;
cluster with_top  ->  non empty for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is with_top holds
not b1 is empty by Def9;
end;

registration
let L be non empty RelStr ;
cluster with_bottom for Element of K32( the carrier of L);
existence
 ex b1 being Subset of L st b1 is with_bottom
proof
take  [#] L ; ::_thesis: [#] L is with_bottom
thus  Bottom L in [#] L ; :: according to WAYBEL23:def_8 ::_thesis: verum
end;
cluster with_top for Element of K32( the carrier of L);
existence
 ex b1 being Subset of L st b1 is with_top
proof
take  [#] L ; ::_thesis: [#] L is with_top
thus  Top L in [#] L ; :: according to WAYBEL23:def_9 ::_thesis: verum
end;
end;

registration
let L be continuous sup-Semilattice;
cluster with_bottom for CLbasis of L;
existence
 ex b1 being CLbasis of L st b1 is with_bottom
proof
A1: now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_((waybelow_x)_/\_([#]_L))
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ ([#] L))
 (waybelow x) /\ ([#] L) = waybelow x by XBOOLE_1:28;
hence  x = sup ((waybelow x) /\ ([#] L)) by WAYBEL_3:def_5; ::_thesis: verum
end;
 for x, y being Element of L st x in [#] L & y in [#] L holds
sup {x,y} in [#] L ;
then  [#] L is join-closed by Th18;
then reconsider S = [#] L as CLbasis of L by A1, Def7;
take  S ; ::_thesis: S is with_bottom
 Bottom L in [#] L ;
hence  S is with_bottom by Def8; ::_thesis: verum
end;
cluster with_top for CLbasis of L;
existence
 ex b1 being CLbasis of L st b1 is with_top
proof
A2: now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_((waybelow_x)_/\_([#]_L))
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ ([#] L))
 (waybelow x) /\ ([#] L) = waybelow x by XBOOLE_1:28;
hence  x = sup ((waybelow x) /\ ([#] L)) by WAYBEL_3:def_5; ::_thesis: verum
end;
 for x, y being Element of L st x in [#] L & y in [#] L holds
sup {x,y} in [#] L ;
then  [#] L is join-closed by Th18;
then reconsider S = [#] L as CLbasis of L by A2, Def7;
take  S ; ::_thesis: S is with_top
 Top L in [#] L ;
hence  S is with_top by Def9; ::_thesis: verum
end;
end;

theorem Th42: :: WAYBEL23:42
for L being non empty antisymmetric lower-bounded RelStr
for S being with_bottom Subset of L holds subrelstr S is lower-bounded
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for S being with_bottom Subset of L holds subrelstr S is lower-bounded
let S be with_bottom Subset of L; ::_thesis: subrelstr S is lower-bounded
 Bottom L in S by Def8;
then reconsider dL = Bottom L as Element of (subrelstr S) by YELLOW_0:def_15;
take  dL ; :: according to YELLOW_0:def_4 ::_thesis: dL is_<=_than the carrier of (subrelstr S)
now__::_thesis:_for_x_being_Element_of_(subrelstr_S)_st_x_in_the_carrier_of_(subrelstr_S)_holds_
dL_<=_x
let x be Element of (subrelstr S); ::_thesis: ( x in the carrier of (subrelstr S) implies dL <= x )
assume  x in the carrier of (subrelstr S) ; ::_thesis: dL <= x
reconsider x1 = x as Element of L by YELLOW_0:58;
 Bottom L <= x1 by YELLOW_0:44;
hence  dL <= x by YELLOW_0:60; ::_thesis: verum
end;
hence  dL is_<=_than the carrier of (subrelstr S) by LATTICE3:def_8; ::_thesis: verum
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
let S be with_bottom Subset of L;
cluster subrelstr S ->  lower-bounded ;
coherence
 subrelstr S is lower-bounded by Th42;
end;

registration
let L be continuous sup-Semilattice;
cluster  ->  join-closed for CLbasis of L;
coherence
 for b1 being CLbasis of L holds b1 is join-closed by Def7;
end;

registration
cluster non empty non trivial reflexive transitive antisymmetric upper-bounded bounded with_suprema with_infima up-complete satisfying_axiom_of_approximation continuous for RelStr ;
existence
 ex b1 being continuous LATTICE st
( b1 is bounded & not b1 is trivial )
proof
set X = the non empty set ;
take  BoolePoset the non empty set ; ::_thesis: ( BoolePoset the non empty set is bounded & not BoolePoset the non empty set is trivial )
thus  ( BoolePoset the non empty set is bounded & not BoolePoset the non empty set is trivial ) ; ::_thesis: verum
end;
end;

registration
let L be non trivial lower-bounded continuous sup-Semilattice;
cluster  ->  non empty for CLbasis of L;
coherence
 for b1 being CLbasis of L holds not b1 is empty
proof
let B be CLbasis of L; ::_thesis: not B is empty
assume A1: B is empty ; ::_thesis: contradiction
Top L = "\/" (((waybelow (Top L)) /\ B),L) by Def7
.= Bottom L by A1 ;
hence  contradiction by WAYBEL_7:3; ::_thesis: verum
end;
end;

theorem Th43: :: WAYBEL23:43
for L being sup-Semilattice holds the carrier of (CompactSublatt L) is join-closed Subset of L
proof
let L be sup-Semilattice; ::_thesis: the carrier of (CompactSublatt L) is join-closed Subset of L
reconsider C = the carrier of (CompactSublatt L) as Subset of L by YELLOW_0:def_13;
 subrelstr C = CompactSublatt L by YELLOW_0:def_15;
hence  the carrier of (CompactSublatt L) is join-closed Subset of L by Def2; ::_thesis: verum
end;

theorem Th44: :: WAYBEL23:44
for L being lower-bounded algebraic LATTICE holds the carrier of (CompactSublatt L) is with_bottom CLbasis of L
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: the carrier of (CompactSublatt L) is with_bottom CLbasis of L
reconsider C = the carrier of (CompactSublatt L) as join-closed Subset of L by Th43;
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_((waybelow_x)_/\_C)
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ C)
 x = sup (compactbelow x) by WAYBEL_8:def_3;
hence  x = sup ((waybelow x) /\ C) by Th1; ::_thesis: verum
end;
then reconsider C = C as CLbasis of L by Def7;
 Bottom L in C by WAYBEL_8:3;
hence  the carrier of (CompactSublatt L) is with_bottom CLbasis of L by Def8; ::_thesis: verum
end;

theorem :: WAYBEL23:45
for L being lower-bounded continuous sup-Semilattice st the carrier of (CompactSublatt L) is CLbasis of L holds
L is algebraic
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: ( the carrier of (CompactSublatt L) is CLbasis of L implies L is algebraic )
reconsider C = the carrier of (CompactSublatt L) as Subset of L by Th43;
assume A1: the carrier of (CompactSublatt L) is CLbasis of L ; ::_thesis: L is algebraic
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(compactbelow_x)
let x be Element of L; ::_thesis: x = sup (compactbelow x)
 x = sup ((waybelow x) /\ C) by A1, Def7;
hence  x = sup (compactbelow x) by Th1; ::_thesis: verum
end;
then A2: L is satisfying_axiom_K by WAYBEL_8:def_3;
 for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ;
hence  L is algebraic by A2, WAYBEL_8:def_4; ::_thesis: verum
end;

theorem Th46: :: WAYBEL23:46
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L holds
( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being join-closed Subset of L holds
( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) )
let B be join-closed Subset of L; ::_thesis: ( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) )
thus  ( B is CLbasis of L implies for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) ) ::_thesis: ( ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) ) implies B is CLbasis of L )
proof
assume A1: B is CLbasis of L ; ::_thesis: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
let x, y be Element of L; ::_thesis: ( not y <= x implies ex b being Element of L st
( b in B & not b <= x & b << y ) )
assume A2: not y <= x ; ::_thesis: ex b being Element of L st
( b in B & not b <= x & b << y )
thus  ex b being Element of L st
( b in B & not b <= x & b << y ) ::_thesis: verum
proof
assume A3: for b1 being Element of L holds
( not b1 in B or b1 <= x or not b1 << y ) ; ::_thesis: contradiction
A4: (waybelow y) /\ B c= downarrow x
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (waybelow y) /\ B or z in downarrow x )
assume A5: z in (waybelow y) /\ B ; ::_thesis: z in downarrow x
then reconsider z1 = z as Element of L ;
 z in waybelow y by A5, XBOOLE_0:def_4;
then A6: z1 << y by WAYBEL_3:7;
 z in B by A5, XBOOLE_0:def_4;
then  z1 <= x by A3, A6;
hence  z in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
A7: ex_sup_of downarrow x,L by YELLOW_0:17;
 ex_sup_of (waybelow y) /\ B,L by YELLOW_0:17;
then  sup ((waybelow y) /\ B) <= sup (downarrow x) by A7, A4, YELLOW_0:34;
then  y <= sup (downarrow x) by A1, Def7;
hence  contradiction by A2, WAYBEL_0:34; ::_thesis: verum
end;
end;
assume A8: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) ; ::_thesis: B is CLbasis of L
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_((waybelow_x)_/\_B)
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ B)
A9: ex_sup_of waybelow x,L by YELLOW_0:17;
 ex_sup_of (waybelow x) /\ B,L by YELLOW_0:17;
then A10: sup ((waybelow x) /\ B) <= sup (waybelow x) by A9, XBOOLE_1:17, YELLOW_0:34;
A11: x <= sup ((waybelow x) /\ B)
proof
assume  not x <= sup ((waybelow x) /\ B) ; ::_thesis: contradiction
then consider b being Element of L such that
A12: b in B and
A13: not b <= sup ((waybelow x) /\ B) and
A14: b << x by A8;
 b in waybelow x by A14, WAYBEL_3:7;
then  b in (waybelow x) /\ B by A12, XBOOLE_0:def_4;
hence  contradiction by A13, YELLOW_2:22; ::_thesis: verum
end;
 x = sup (waybelow x) by WAYBEL_3:def_5;
hence  x = sup ((waybelow x) /\ B) by A10, A11, YELLOW_0:def_3; ::_thesis: verum
end;
hence  B is CLbasis of L by Def7; ::_thesis: verum
end;

theorem Th47: :: WAYBEL23:47
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) )
let B be join-closed Subset of L; ::_thesis: ( Bottom L in B implies ( B is CLbasis of L iff for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) )
assume A1: Bottom L in B ; ::_thesis: ( B is CLbasis of L iff for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) )
thus  ( B is CLbasis of L implies for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) ::_thesis: ( ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) implies B is CLbasis of L )
proof
assume A2: B is CLbasis of L ; ::_thesis: for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y )
let x, y be Element of L; ::_thesis: ( x << y implies ex b being Element of L st
( b in B & x <= b & b << y ) )
assume A3: x << y ; ::_thesis: ex b being Element of L st
( b in B & x <= b & b << y )
 Bottom L << y by WAYBEL_3:4;
then A4: Bottom L in waybelow y by WAYBEL_3:7;
 (waybelow y) /\ B is join-closed by Th33;
then reconsider D = (waybelow y) /\ B as non empty directed Subset of L by A1, A4, XBOOLE_0:def_4;
 y = sup D by A2, Def7;
then consider b being Element of L such that
A5: b in D and
A6: x <= b by A3, WAYBEL_3:def_1;
take  b ; ::_thesis: ( b in B & x <= b & b << y )
 b in waybelow y by A5, XBOOLE_0:def_4;
hence  ( b in B & x <= b & b << y ) by A5, A6, WAYBEL_3:7, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A7: for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ; ::_thesis: B is CLbasis of L
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_((waybelow_x)_/\_B)
let x be Element of L; ::_thesis: x = sup ((waybelow x) /\ B)
A8: x <= sup ((waybelow x) /\ B)
proof
A9: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;
assume  not x <= sup ((waybelow x) /\ B) ; ::_thesis: contradiction
then consider u being Element of L such that
A10: u << x and
A11: not u <= sup ((waybelow x) /\ B) by A9, WAYBEL_3:24;
consider b being Element of L such that
A12: b in B and
A13: u <= b and
A14: b << x by A7, A10;
 b in waybelow x by A14, WAYBEL_3:7;
then A15: b in (waybelow x) /\ B by A12, XBOOLE_0:def_4;
A16: sup ((waybelow x) /\ B) is_>=_than (waybelow x) /\ B by YELLOW_0:32;
 not b <= sup ((waybelow x) /\ B) by A11, A13, YELLOW_0:def_2;
hence  contradiction by A15, A16, LATTICE3:def_9; ::_thesis: verum
end;
 (waybelow x) /\ B c= waybelow x by XBOOLE_1:17;
then  sup ((waybelow x) /\ B) <= sup (waybelow x) by WAYBEL_7:1;
then  sup ((waybelow x) /\ B) <= x by WAYBEL_3:def_5;
hence  x = sup ((waybelow x) /\ B) by A8, YELLOW_0:def_3; ::_thesis: verum
end;
hence  B is CLbasis of L by Def7; ::_thesis: verum
end;

Lm2:  for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) holds
( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) holds
( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
let B be join-closed Subset of L; ::_thesis: ( Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) implies ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
assume A1: Bottom L in B ; ::_thesis: ( ex x, y being Element of L st
( x << y & ( for b being Element of L holds
( not b in B or not x <= b or not b << y ) ) ) or ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
assume A2: for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ; ::_thesis: ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
thus  the carrier of (CompactSublatt L) c= B ::_thesis: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y )
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of (CompactSublatt L) or z in B )
assume A3: z in the carrier of (CompactSublatt L) ; ::_thesis: z in B
 the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def_13;
then reconsider z1 = z as Element of L by A3;
 z1 is compact by A3, WAYBEL_8:def_1;
then  z1 << z1 by WAYBEL_3:def_2;
then consider b being Element of L such that
A4: b in B and
A5: z1 <= b and
A6: b << z1 by A2;
 b <= z1 by A6, WAYBEL_3:1;
hence  z in B by A4, A5, YELLOW_0:def_3; ::_thesis: verum
end;
let x, y be Element of L; ::_thesis: ( not y <= x implies ex b being Element of L st
( b in B & not b <= x & b <= y ) )
assume A7: not y <= x ; ::_thesis: ex b being Element of L st
( b in B & not b <= x & b <= y )
 B is CLbasis of L by A1, A2, Th47;
then consider b being Element of L such that
A8: b in B and
A9: not b <= x and
A10: b << y by A7, Th46;
take  b ; ::_thesis: ( b in B & not b <= x & b <= y )
thus  ( b in B & not b <= x & b <= y ) by A8, A9, A10, WAYBEL_3:1; ::_thesis: verum
end;

Lm3:  for L being lower-bounded continuous LATTICE
for B being Subset of L st ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) holds
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being Subset of L st ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) holds
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
let B be Subset of L; ::_thesis: ( ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) implies for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) )
assume A1: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ; ::_thesis: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
let x, y be Element of L; ::_thesis: ( not y <= x implies ex b being Element of L st
( b in B & not b <= x & b << y ) )
A2: for z being Element of L holds
( not waybelow z is empty & waybelow z is directed ) ;
assume  not y <= x ; ::_thesis: ex b being Element of L st
( b in B & not b <= x & b << y )
then consider y1 being Element of L such that
A3: y1 << y and
A4: not y1 <= x by A2, WAYBEL_3:24;
consider b being Element of L such that
A5: b in B and
A6: not b <= x and
A7: b <= y1 by A1, A4;
take  b ; ::_thesis: ( b in B & not b <= x & b << y )
thus  ( b in B & not b <= x & b << y ) by A3, A5, A6, A7, WAYBEL_3:2; ::_thesis: verum
end;

theorem Th48: :: WAYBEL23:48
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
let B be join-closed Subset of L; ::_thesis: ( Bottom L in B implies ( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) ) )
assume A1: Bottom L in B ; ::_thesis: ( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
thus  ( B is CLbasis of L implies ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) ) ::_thesis: ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) implies B is CLbasis of L )
proof
assume  B is CLbasis of L ; ::_thesis: ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
then  for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) by A1, Th47;
hence  ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) by A1, Lm2; ::_thesis: verum
end;
assume that
 the carrier of (CompactSublatt L) c= B and
A2: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ; ::_thesis: B is CLbasis of L
 for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) by A2, Lm3;
hence  B is CLbasis of L by Th46; ::_thesis: verum
end;

theorem :: WAYBEL23:49
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) )
let B be join-closed Subset of L; ::_thesis: ( Bottom L in B implies ( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
assume A1: Bottom L in B ; ::_thesis: ( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) )
thus  ( B is CLbasis of L implies for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ::_thesis: ( ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) implies B is CLbasis of L )
proof
assume  B is CLbasis of L ; ::_thesis: for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y )
then  for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) by A1, Th47;
hence  for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) by A1, Lm2; ::_thesis: verum
end;
assume  for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ; ::_thesis: B is CLbasis of L
then  for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y ) by Lm3;
hence  B is CLbasis of L by Th46; ::_thesis: verum
end;

theorem Th50: :: WAYBEL23:50
for L being lower-bounded sup-Semilattice
for S being non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L holds
for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for S being non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L holds
for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S
let S be non empty full SubRelStr of L; ::_thesis: ( Bottom L in the carrier of S & the carrier of S is join-closed Subset of L implies for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S )
assume that
A1: Bottom L in the carrier of S and
A2: the carrier of S is join-closed Subset of L ; ::_thesis: for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S
let x be Element of L; ::_thesis: (waybelow x) /\ the carrier of S is Ideal of S
 Bottom L << x by WAYBEL_3:4;
then  Bottom L in waybelow x by WAYBEL_3:7;
then reconsider X = (waybelow x) /\ the carrier of S as non empty Subset of S by A1, XBOOLE_0:def_4, XBOOLE_1:17;
reconsider S1 = the carrier of S as join-closed Subset of L by A2;
A3: now__::_thesis:_for_a,_b_being_Element_of_S_st_a_in_X_&_b_<=_a_holds_
b_in_X
let a, b be Element of S; ::_thesis: ( a in X & b <= a implies b in X )
reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;
assume that
A4: a in X and
A5: b <= a ; ::_thesis: b in X
 a in waybelow x by A4, XBOOLE_0:def_4;
then A6: a1 << x by WAYBEL_3:7;
 b1 <= a1 by A5, YELLOW_0:59;
then  b1 << x by A6, WAYBEL_3:2;
then  b in waybelow x by WAYBEL_3:7;
hence  b in X by XBOOLE_0:def_4; ::_thesis: verum
end;
 (waybelow x) /\ S1 is join-closed by Th33;
hence  (waybelow x) /\ the carrier of S is Ideal of S by A3, WAYBEL10:23, WAYBEL_0:def_19; ::_thesis: verum
end;

definition
let L be non empty reflexive transitive RelStr ;
let S be non empty full SubRelStr of L;
func supMap S ->  Function of (InclPoset (Ids S)),L means :Def10: :: WAYBEL23:def 10
 for I being Ideal of S holds it . I = "\/" (I,L);
existence
 ex b1 being Function of (InclPoset (Ids S)),L st
for I being Ideal of S holds b1 . I = "\/" (I,L)
proof
deffunc H1( set ) ->  Element of the carrier of L = "\/" ($1,L);
set P = InclPoset (Ids S);
A1: for I being set st I in the carrier of (InclPoset (Ids S)) holds
H1(I) in the carrier of L ;
 ex f being Function of the carrier of (InclPoset (Ids S)), the carrier of L st
for I being set st I in the carrier of (InclPoset (Ids S)) holds
f . I = H1(I) from FUNCT_2:sch_2(A1);
then consider f being Function of the carrier of (InclPoset (Ids S)), the carrier of L such that
A2: for I being set st I in the carrier of (InclPoset (Ids S)) holds
f . I = "\/" (I,L) ;
reconsider f = f as Function of (InclPoset (Ids S)),L ;
take  f ; ::_thesis: for I being Ideal of S holds f . I = "\/" (I,L)
 for I being Ideal of S holds f . I = "\/" (I,L)
proof
let I be Ideal of S; ::_thesis: f . I = "\/" (I,L)
 I in  {  X where X is Ideal of S : verum  }  ;
then  I in the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by WAYBEL_0:def_23;
then  I in the carrier of (InclPoset (Ids S)) by YELLOW_1:def_1;
hence  f . I = "\/" (I,L) by A2; ::_thesis: verum
end;
hence  for I being Ideal of S holds f . I = "\/" (I,L) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (InclPoset (Ids S)),L st ( for I being Ideal of S holds b1 . I = "\/" (I,L) ) & ( for I being Ideal of S holds b2 . I = "\/" (I,L) ) holds
b1 = b2
proof
set P = InclPoset (Ids S);
let f, g be Function of (InclPoset (Ids S)),L; ::_thesis: ( ( for I being Ideal of S holds f . I = "\/" (I,L) ) & ( for I being Ideal of S holds g . I = "\/" (I,L) ) implies f = g )
assume that
A3: for I being Ideal of S holds f . I = "\/" (I,L) and
A4: for I being Ideal of S holds g . I = "\/" (I,L) ; ::_thesis: f = g
A5: the carrier of (InclPoset (Ids S)) = the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def_1
.= Ids S ;
A6: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(InclPoset_(Ids_S))_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of (InclPoset (Ids S)) implies f . x = g . x )
assume  x in the carrier of (InclPoset (Ids S)) ; ::_thesis: f . x = g . x
then  x in  {  X where X is Ideal of S : verum  }  by A5, WAYBEL_0:def_23;
then  ex I being Ideal of S st x = I ;
then reconsider I = x as Ideal of S ;
 f . I = "\/" (I,L) by A3;
hence  f . x = g . x by A4; ::_thesis: verum
end;
A7: dom g = the carrier of (InclPoset (Ids S)) by FUNCT_2:def_1;
 dom f = the carrier of (InclPoset (Ids S)) by FUNCT_2:def_1;
hence  f = g by A7, A6, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines supMap WAYBEL23:def_10_:_
 for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for b3 being Function of (InclPoset (Ids S)),L holds
( b3 = supMap S iff for I being Ideal of S holds b3 . I = "\/" (I,L) );

definition
let L be non empty reflexive transitive RelStr ;
let S be non empty full SubRelStr of L;
func idsMap S ->  Function of (InclPoset (Ids S)),(InclPoset (Ids L)) means :Def11: :: WAYBEL23:def 11
 for I being Ideal of S ex J being Subset of L st
( I = J & it . I = downarrow J );
existence
 ex b1 being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) st
for I being Ideal of S ex J being Subset of L st
( I = J & b1 . I = downarrow J )
proof
defpred S1[ set , set ] means  ex J being Subset of L st
( $1 = J & $2 = downarrow J );
set R = InclPoset (Ids L);
set P = InclPoset (Ids S);
A1: for I being Element of (InclPoset (Ids S)) ex K being Element of (InclPoset (Ids L)) st S1[I,K]
proof
let I be Element of (InclPoset (Ids S)); ::_thesis: ex K being Element of (InclPoset (Ids L)) st S1[I,K]
 I in the carrier of (InclPoset (Ids S)) ;
then  I in Ids S by YELLOW_1:1;
then  I in  {  X where X is Ideal of S : verum  }  by WAYBEL_0:def_23;
then consider J being Ideal of S such that
A2: J = I ;
reconsider J = J as non empty directed Subset of L by YELLOW_2:7;
 downarrow J in  {  X where X is Ideal of L : verum  }  ;
then  downarrow J in Ids L by WAYBEL_0:def_23;
then reconsider K = downarrow J as Element of (InclPoset (Ids L)) by YELLOW_1:1;
take  K ; ::_thesis: S1[I,K]
take  J ; ::_thesis: ( I = J & K = downarrow J )
thus  ( I = J & K = downarrow J ) by A2; ::_thesis: verum
end;
 ex f being Function of the carrier of (InclPoset (Ids S)), the carrier of (InclPoset (Ids L)) st
for I being Element of (InclPoset (Ids S)) holds S1[I,f . I] from FUNCT_2:sch_3(A1);
then consider f being Function of the carrier of (InclPoset (Ids S)), the carrier of (InclPoset (Ids L)) such that
A3: for I being Element of (InclPoset (Ids S)) ex J being Subset of L st
( I = J & f . I = downarrow J ) ;
reconsider f = f as Function of (InclPoset (Ids S)),(InclPoset (Ids L)) ;
take  f ; ::_thesis: for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J )
 for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J )
proof
let I be Ideal of S; ::_thesis: ex J being Subset of L st
( I = J & f . I = downarrow J )
 I in  {  X where X is Ideal of S : verum  }  ;
then  I in the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by WAYBEL_0:def_23;
then  I in the carrier of (InclPoset (Ids S)) by YELLOW_1:def_1;
then consider J being Subset of L such that
A4: I = J and
A5: f . I = downarrow J by A3;
reconsider J = J as Subset of L ;
take  J ; ::_thesis: ( I = J & f . I = downarrow J )
thus  ( I = J & f . I = downarrow J ) by A4, A5; ::_thesis: verum
end;
hence  for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) st ( for I being Ideal of S ex J being Subset of L st
( I = J & b1 . I = downarrow J ) ) & ( for I being Ideal of S ex J being Subset of L st
( I = J & b2 . I = downarrow J ) ) holds
b1 = b2
proof
set P = InclPoset (Ids S);
let f, g be Function of (InclPoset (Ids S)),(InclPoset (Ids L)); ::_thesis: ( ( for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J ) ) & ( for I being Ideal of S ex J being Subset of L st
( I = J & g . I = downarrow J ) ) implies f = g )
assume that
A6: for I being Ideal of S ex J being Subset of L st
( I = J & f . I = downarrow J ) and
A7: for I being Ideal of S ex J being Subset of L st
( I = J & g . I = downarrow J ) ; ::_thesis: f = g
A8: the carrier of (InclPoset (Ids S)) = the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def_1
.= Ids S ;
A9: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(InclPoset_(Ids_S))_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of (InclPoset (Ids S)) implies f . x = g . x )
assume  x in the carrier of (InclPoset (Ids S)) ; ::_thesis: f . x = g . x
then  x in  {  X where X is Ideal of S : verum  }  by A8, WAYBEL_0:def_23;
then  ex I being Ideal of S st x = I ;
then reconsider I = x as Ideal of S ;
A10: ex J2 being Subset of L st
( I = J2 & g . I = downarrow J2 ) by A7;
 ex J1 being Subset of L st
( I = J1 & f . I = downarrow J1 ) by A6;
hence  f . x = g . x by A10; ::_thesis: verum
end;
A11: dom g = the carrier of (InclPoset (Ids S)) by FUNCT_2:def_1;
 dom f = the carrier of (InclPoset (Ids S)) by FUNCT_2:def_1;
hence  f = g by A11, A9, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines idsMap WAYBEL23:def_11_:_
 for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for b3 being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) holds
( b3 = idsMap S iff for I being Ideal of S ex J being Subset of L st
( I = J & b3 . I = downarrow J ) );

registration
let L be reflexive RelStr ;
let B be Subset of L;
cluster subrelstr B ->  reflexive ;
coherence
 subrelstr B is reflexive ;
end;

registration
let L be transitive RelStr ;
let B be Subset of L;
cluster subrelstr B ->  transitive ;
coherence
 subrelstr B is transitive ;
end;

registration
let L be antisymmetric RelStr ;
let B be Subset of L;
cluster subrelstr B ->  antisymmetric ;
coherence
 subrelstr B is antisymmetric ;
end;

definition
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
func baseMap B ->  Function of L,(InclPoset (Ids (subrelstr B))) means :Def12: :: WAYBEL23:def 12
 for x being Element of L holds it . x = (waybelow x) /\ B;
existence
 ex b1 being Function of L,(InclPoset (Ids (subrelstr B))) st
for x being Element of L holds b1 . x = (waybelow x) /\ B
proof
defpred S1[ set , set ] means  ex y being Element of L st
( $1 = y & $2 = (waybelow y) /\ B );
set P = InclPoset (Ids (subrelstr B));
A1: for x being Element of L ex z being Element of (InclPoset (Ids (subrelstr B))) st S1[x,z]
proof
let x be Element of L; ::_thesis: ex z being Element of (InclPoset (Ids (subrelstr B))) st S1[x,z]
reconsider y = x as Element of L ;
A2: the carrier of (subrelstr B) = B by YELLOW_0:def_15;
 Bottom L in B by Def8;
then  (waybelow y) /\ B is Ideal of (subrelstr B) by A2, Th50;
then reconsider z = (waybelow y) /\ B as Element of (InclPoset (Ids (subrelstr B))) by YELLOW_2:41;
take  z ; ::_thesis: S1[x,z]
take  y ; ::_thesis: ( x = y & z = (waybelow y) /\ B )
thus  ( x = y & z = (waybelow y) /\ B ) ; ::_thesis: verum
end;
 ex f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) st
for x being Element of L holds S1[x,f . x] from FUNCT_2:sch_3(A1);
then consider f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) such that
A3: for x being Element of L ex y being Element of L st
( x = y & f . x = (waybelow y) /\ B ) ;
reconsider f = f as Function of L,(InclPoset (Ids (subrelstr B))) ;
take  f ; ::_thesis: for x being Element of L holds f . x = (waybelow x) /\ B
now__::_thesis:_for_x_being_Element_of_L_holds_f_._x_=_(waybelow_x)_/\_B
let x be Element of L; ::_thesis: f . x = (waybelow x) /\ B
 ex y being Element of L st
( x = y & f . x = (waybelow y) /\ B ) by A3;
hence  f . x = (waybelow x) /\ B ; ::_thesis: verum
end;
hence  for x being Element of L holds f . x = (waybelow x) /\ B ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of L,(InclPoset (Ids (subrelstr B))) st ( for x being Element of L holds b1 . x = (waybelow x) /\ B ) & ( for x being Element of L holds b2 . x = (waybelow x) /\ B ) holds
b1 = b2
proof
let f, g be Function of L,(InclPoset (Ids (subrelstr B))); ::_thesis: ( ( for x being Element of L holds f . x = (waybelow x) /\ B ) & ( for x being Element of L holds g . x = (waybelow x) /\ B ) implies f = g )
assume that
A4: for x being Element of L holds f . x = (waybelow x) /\ B and
A5: for x being Element of L holds g . x = (waybelow x) /\ B ; ::_thesis: f = g
A6: now__::_thesis:_for_z_being_set_st_z_in_the_carrier_of_L_holds_
f_._z_=_g_._z
let z be set ; ::_thesis: ( z in the carrier of L implies f . z = g . z )
assume  z in the carrier of L ; ::_thesis: f . z = g . z
then reconsider z1 = z as Element of L ;
 f . z = (waybelow z1) /\ B by A4;
hence  f . z = g . z by A5; ::_thesis: verum
end;
A7: dom g = the carrier of L by FUNCT_2:def_1;
 dom f = the carrier of L by FUNCT_2:def_1;
hence  f = g by A7, A6, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines baseMap WAYBEL23:def_12_:_
 for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L
for b3 being Function of L,(InclPoset (Ids (subrelstr B))) holds
( b3 = baseMap B iff for x being Element of L holds b3 . x = (waybelow x) /\ B );

theorem Th51: :: WAYBEL23:51
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds
( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L holds
( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )
let S be non empty full SubRelStr of L; ::_thesis: ( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )
set P = InclPoset (Ids S);
thus  dom (supMap S) = the carrier of (InclPoset (Ids S)) by FUNCT_2:def_1
.= the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def_1
.= Ids S ; ::_thesis: rng (supMap S) is Subset of L
thus  rng (supMap S) is Subset of L ; ::_thesis: verum
end;

theorem Th52: :: WAYBEL23:52
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set holds
( x in dom (supMap S) iff x is Ideal of S )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L
for x being set holds
( x in dom (supMap S) iff x is Ideal of S )
let S be non empty full SubRelStr of L; ::_thesis: for x being set holds
( x in dom (supMap S) iff x is Ideal of S )
let x be set ; ::_thesis: ( x in dom (supMap S) iff x is Ideal of S )
hereby  ::_thesis: ( x is Ideal of S implies x in dom (supMap S) )
assume  x in dom (supMap S) ; ::_thesis: x is Ideal of S
then  x in Ids S by Th51;
then  x in  {  X where X is Ideal of S : verum  }  by WAYBEL_0:def_23;
then  ex I being Ideal of S st x = I ;
hence  x is Ideal of S ; ::_thesis: verum
end;
assume  x is Ideal of S ; ::_thesis: x in dom (supMap S)
then  x in  {  X where X is Ideal of S : verum  }  ;
then  x in Ids S by WAYBEL_0:def_23;
hence  x in dom (supMap S) by Th51; ::_thesis: verum
end;

theorem Th53: :: WAYBEL23:53
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds
( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L holds
( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )
let S be non empty full SubRelStr of L; ::_thesis: ( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )
set P = InclPoset (Ids S);
thus  dom (idsMap S) = the carrier of (InclPoset (Ids S)) by FUNCT_2:def_1
.= the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def_1
.= Ids S ; ::_thesis: rng (idsMap S) is Subset of (Ids L)
thus  rng (idsMap S) is Subset of (Ids L) by YELLOW_1:1; ::_thesis: verum
end;

theorem Th54: :: WAYBEL23:54
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set holds
( x in dom (idsMap S) iff x is Ideal of S )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L
for x being set holds
( x in dom (idsMap S) iff x is Ideal of S )
let S be non empty full SubRelStr of L; ::_thesis: for x being set holds
( x in dom (idsMap S) iff x is Ideal of S )
let x be set ; ::_thesis: ( x in dom (idsMap S) iff x is Ideal of S )
hereby  ::_thesis: ( x is Ideal of S implies x in dom (idsMap S) )
assume  x in dom (idsMap S) ; ::_thesis: x is Ideal of S
then  x in Ids S by Th53;
then  x in  {  X where X is Ideal of S : verum  }  by WAYBEL_0:def_23;
then  ex I being Ideal of S st x = I ;
hence  x is Ideal of S ; ::_thesis: verum
end;
assume  x is Ideal of S ; ::_thesis: x in dom (idsMap S)
then  x in  {  X where X is Ideal of S : verum  }  ;
then  x in Ids S by WAYBEL_0:def_23;
hence  x in dom (idsMap S) by Th53; ::_thesis: verum
end;

theorem Th55: :: WAYBEL23:55
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set st x in rng (idsMap S) holds
x is Ideal of L
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L
for x being set st x in rng (idsMap S) holds
x is Ideal of L
let S be non empty full SubRelStr of L; ::_thesis: for x being set st x in rng (idsMap S) holds
x is Ideal of L
let x be set ; ::_thesis: ( x in rng (idsMap S) implies x is Ideal of L )
assume A1: x in rng (idsMap S) ; ::_thesis: x is Ideal of L
 rng (idsMap S) is Subset of (Ids L) by Th53;
then  x in Ids L by A1;
then  x in  {  X where X is Ideal of L : verum  }  by WAYBEL_0:def_23;
then  ex I being Ideal of L st x = I ;
hence  x is Ideal of L ; ::_thesis: verum
end;

theorem :: WAYBEL23:56
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( dom (baseMap B) = the carrier of L & rng (baseMap B) is Subset of (Ids (subrelstr B)) ) by FUNCT_2:def_1, YELLOW_1:1;

theorem :: WAYBEL23:57
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L
for x being set st x in rng (baseMap B) holds
x is Ideal of (subrelstr B)
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L
for x being set st x in rng (baseMap B) holds
x is Ideal of (subrelstr B)
let B be with_bottom CLbasis of L; ::_thesis: for x being set st x in rng (baseMap B) holds
x is Ideal of (subrelstr B)
let x be set ; ::_thesis: ( x in rng (baseMap B) implies x is Ideal of (subrelstr B) )
A1: rng (baseMap B) is Subset of (Ids (subrelstr B)) by YELLOW_1:1;
assume  x in rng (baseMap B) ; ::_thesis: x is Ideal of (subrelstr B)
then  x in Ids (subrelstr B) by A1;
then  x in  {  X where X is Ideal of (subrelstr B) : verum  }  by WAYBEL_0:def_23;
then  ex I being Ideal of (subrelstr B) st x = I ;
hence  x is Ideal of (subrelstr B) ; ::_thesis: verum
end;

theorem Th58: :: WAYBEL23:58
for L being non empty up-complete Poset
for S being non empty full SubRelStr of L holds supMap S is monotone
proof
let L be non empty up-complete Poset; ::_thesis: for S being non empty full SubRelStr of L holds supMap S is monotone
let S be non empty full SubRelStr of L; ::_thesis: supMap S is monotone
set f = supMap S;
now__::_thesis:_for_x,_y_being_Element_of_(InclPoset_(Ids_S))_st_x_<=_y_holds_
(supMap_S)_._x_<=_(supMap_S)_._y
let x, y be Element of (InclPoset (Ids S)); ::_thesis: ( x <= y implies (supMap S) . x <= (supMap S) . y )
reconsider I = x, J = y as Ideal of S by YELLOW_2:41;
assume  x <= y ; ::_thesis: (supMap S) . x <= (supMap S) . y
then A1: I c= J by YELLOW_1:3;
 I is non empty directed Subset of L by YELLOW_2:7;
then A2: ex_sup_of I,L by WAYBEL_0:75;
 J is non empty directed Subset of L by YELLOW_2:7;
then A3: ex_sup_of J,L by WAYBEL_0:75;
A4: (supMap S) . y = "\/" (J,L) by Def10;
 (supMap S) . x = "\/" (I,L) by Def10;
hence  (supMap S) . x <= (supMap S) . y by A2, A3, A1, A4, YELLOW_0:34; ::_thesis: verum
end;
hence  supMap S is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;

theorem Th59: :: WAYBEL23:59
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds idsMap S is monotone
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L holds idsMap S is monotone
let S be non empty full SubRelStr of L; ::_thesis: idsMap S is monotone
set f = idsMap S;
now__::_thesis:_for_x,_y_being_Element_of_(InclPoset_(Ids_S))_st_x_<=_y_holds_
(idsMap_S)_._x_<=_(idsMap_S)_._y
let x, y be Element of (InclPoset (Ids S)); ::_thesis: ( x <= y implies (idsMap S) . x <= (idsMap S) . y )
reconsider I = x, J = y as Ideal of S by YELLOW_2:41;
consider K1 being Subset of L such that
A1: I = K1 and
A2: (idsMap S) . x = downarrow K1 by Def11;
consider K2 being Subset of L such that
A3: J = K2 and
A4: (idsMap S) . y = downarrow K2 by Def11;
assume  x <= y ; ::_thesis: (idsMap S) . x <= (idsMap S) . y
then  I c= J by YELLOW_1:3;
then  downarrow K1 c= downarrow K2 by A1, A3, YELLOW_3:6;
hence  (idsMap S) . x <= (idsMap S) . y by A2, A4, YELLOW_1:3; ::_thesis: verum
end;
hence  idsMap S is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;

theorem Th60: :: WAYBEL23:60
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds baseMap B is monotone
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds baseMap B is monotone
let B be with_bottom CLbasis of L; ::_thesis: baseMap B is monotone
set f = baseMap B;
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_<=_y_holds_
(baseMap_B)_._x_<=_(baseMap_B)_._y
let x, y be Element of L; ::_thesis: ( x <= y implies (baseMap B) . x <= (baseMap B) . y )
assume A1: x <= y ; ::_thesis: (baseMap B) . x <= (baseMap B) . y
A2: (baseMap B) . y = (waybelow y) /\ B by Def12;
 (baseMap B) . x = (waybelow x) /\ B by Def12;
then  (baseMap B) . x c= (baseMap B) . y by A1, A2, WAYBEL_3:12, XBOOLE_1:26;
hence  (baseMap B) . x <= (baseMap B) . y by YELLOW_1:3; ::_thesis: verum
end;
hence  baseMap B is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;

registration
let L be non empty up-complete Poset;
let S be non empty full SubRelStr of L;
cluster supMap S ->  monotone ;
coherence
 supMap S is monotone by Th58;
end;

registration
let L be non empty reflexive transitive RelStr ;
let S be non empty full SubRelStr of L;
cluster idsMap S ->  monotone ;
coherence
 idsMap S is monotone by Th59;
end;

registration
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster baseMap B ->  monotone ;
coherence
 baseMap B is monotone by Th60;
end;

theorem Th61: :: WAYBEL23:61
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving
let B be with_bottom CLbasis of L; ::_thesis: idsMap (subrelstr B) is sups-preserving
set f = idsMap (subrelstr B);
A1: subrelstr B is join-inheriting by Def2;
A2: Bottom L in B by Def8;
then A3: Bottom L in the carrier of (subrelstr B) by YELLOW_0:def_15;
now__::_thesis:_for_X_being_Subset_of_(InclPoset_(Ids_(subrelstr_B)))_holds_idsMap_(subrelstr_B)_preserves_sup_of_X
let X be Subset of (InclPoset (Ids (subrelstr B))); ::_thesis: idsMap (subrelstr B) preserves_sup_of X
reconsider supX = sup X as Ideal of (subrelstr B) by YELLOW_2:41;
reconsider unionX = union X as Subset of L by WAYBEL13:3;
reconsider dfuX = downarrow (finsups (union X)) as Subset of L by WAYBEL13:3;
reconsider fuX = finsups (union X) as Subset of L by WAYBEL13:3;
A4: ex J being Subset of L st
( supX = J & (idsMap (subrelstr B)) . supX = downarrow J ) by Def11;
now__::_thesis:_(_ex_sup_of_X,_InclPoset_(Ids_(subrelstr_B))_implies_(_ex_sup_of_(idsMap_(subrelstr_B))_.:_X,_InclPoset_(Ids_L)_&_sup_((idsMap_(subrelstr_B))_.:_X)_=_(idsMap_(subrelstr_B))_._(sup_X)_)_)
assume  ex_sup_of X, InclPoset (Ids (subrelstr B)) ; ::_thesis: ( ex_sup_of (idsMap (subrelstr B)) .: X, InclPoset (Ids L) & sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X) )
thus  ex_sup_of (idsMap (subrelstr B)) .: X, InclPoset (Ids L) by YELLOW_0:17; ::_thesis: sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X)
A5: downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) c= downarrow dfuX
proof
defpred S1[ set , set ] means  ex I being Element of (InclPoset (Ids (subrelstr B))) ex z1, z2 being Element of L st
( z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2 );
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) or x in downarrow dfuX )
assume A6: x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) ; ::_thesis: x in downarrow dfuX
then reconsider x1 = x as Element of L ;
consider y1 being Element of L such that
A7: y1 >= x1 and
A8: y1 in finsups (union ((idsMap (subrelstr B)) .: X)) by A6, WAYBEL_0:def_15;
 y1 in  {  ("\/" (V,L)) where V is finite Subset of (union ((idsMap (subrelstr B)) .: X)) : ex_sup_of V,L  }  by A8, WAYBEL_0:def_27;
then consider Y being finite Subset of (union ((idsMap (subrelstr B)) .: X)) such that
A9: y1 = "\/" (Y,L) and
 ex_sup_of Y,L ;
A10: for z being set st z in Y holds
ex v being Element of B st S1[z,v]
proof
let z be set ; ::_thesis: ( z in Y implies ex v being Element of B st S1[z,v] )
assume  z in Y ; ::_thesis: ex v being Element of B st S1[z,v]
then consider J being set  such that
A11: z in J and
A12: J in (idsMap (subrelstr B)) .: X by TARSKI:def_4;
consider I being set  such that
 I in dom (idsMap (subrelstr B)) and
A13: I in X and
A14: J = (idsMap (subrelstr B)) . I by A12, FUNCT_1:def_6;
reconsider I = I as Element of (InclPoset (Ids (subrelstr B))) by A13;
 (idsMap (subrelstr B)) . I is Element of (InclPoset (Ids L)) ;
then reconsider J = J as Element of (InclPoset (Ids L)) by A14;
 J is Ideal of L by YELLOW_2:41;
then reconsider z1 = z as Element of L by A11;
reconsider I1 = I as Ideal of (subrelstr B) by YELLOW_2:41;
consider I2 being Subset of L such that
A15: I1 = I2 and
A16: (idsMap (subrelstr B)) . I1 = downarrow I2 by Def11;
consider z2 being Element of L such that
A17: z2 >= z1 and
A18: z2 in I2 by A11, A14, A16, WAYBEL_0:def_15;
reconsider v = z2 as Element of B by A15, A18, YELLOW_0:def_15;
take  v ; ::_thesis: S1[z,v]
take  I ; ::_thesis: ex z1, z2 being Element of L st
( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )
take  z1 ; ::_thesis: ex z2 being Element of L st
( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )
take  z2 ; ::_thesis: ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )
thus  ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 ) by A13, A15, A17, A18; ::_thesis: verum
end;
consider g being Function of Y,B such that
A19: for z being set st z in Y holds
S1[z,g . z] from MONOID_1:sch_1(A10);
reconsider Z = rng g as finite Subset of (subrelstr B) by YELLOW_0:def_15;
A20: dom g = Y by FUNCT_2:def_1;
A21: "\/" ((rng g),L) is_>=_than Y
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in Y or a <= "\/" ((rng g),L) )
A22: "\/" ((rng g),L) is_>=_than rng g by YELLOW_0:32;
assume A23: a in Y ; ::_thesis: a <= "\/" ((rng g),L)
then consider I being Element of (InclPoset (Ids (subrelstr B))), a1, a2 being Element of L such that
A24: a1 = a and
A25: a2 = g . a and
 I in X and
 g . a in I and
A26: a1 <= a2 by A19;
 g . a in rng g by A20, A23, FUNCT_1:def_3;
then  a2 <= "\/" ((rng g),L) by A25, A22, LATTICE3:def_9;
hence  a <= "\/" ((rng g),L) by A24, A26, YELLOW_0:def_2; ::_thesis: verum
end;
A27: ex_sup_of Z, subrelstr B
proof
percases ( not Z is empty or Z is empty ) ;
suppose not Z is empty ; ::_thesis: ex_sup_of Z, subrelstr B
hence  ex_sup_of Z, subrelstr B by YELLOW_0:54; ::_thesis: verum
end;
suppose Z is empty ; ::_thesis: ex_sup_of Z, subrelstr B
hence  ex_sup_of Z, subrelstr B by YELLOW_0:42; ::_thesis: verum
end;
end;
end;
 rng g c= union X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in union X )
assume  a in rng g ; ::_thesis: a in union X
then consider b being set  such that
A28: b in dom g and
A29: a = g . b by FUNCT_1:def_3;
 ex I being Element of (InclPoset (Ids (subrelstr B))) ex b1, b2 being Element of L st
( b1 = b & b2 = g . b & I in X & g . b in I & b1 <= b2 ) by A19, A28;
hence  a in union X by A29, TARSKI:def_4; ::_thesis: verum
end;
then  "\/" (Z,(subrelstr B)) in  {  ("\/" (V,(subrelstr B))) where V is finite Subset of (union X) : ex_sup_of V, subrelstr B  }  by A27;
then A30: "\/" ((rng g),(subrelstr B)) in finsups (union X) by WAYBEL_0:def_27;
 "\/" (Z,L) in the carrier of (subrelstr B)
proof
percases ( not Z is empty or Z is empty ) ;
suppose not Z is empty ; ::_thesis: "\/" (Z,L) in the carrier of (subrelstr B)
hence  "\/" (Z,L) in the carrier of (subrelstr B) by A1, WAYBEL21:15; ::_thesis: verum
end;
suppose Z is empty ; ::_thesis: "\/" (Z,L) in the carrier of (subrelstr B)
hence  "\/" (Z,L) in the carrier of (subrelstr B) by A2, YELLOW_0:def_15; ::_thesis: verum
end;
end;
end;
then reconsider xl = "\/" (Z,L) as Element of (subrelstr B) ;
reconsider srg = "\/" ((rng g),(subrelstr B)) as Element of L by YELLOW_0:58;
A31: ex_sup_of Z,L by YELLOW_0:17;
A32: now__::_thesis:_for_b_being_Element_of_(subrelstr_B)_st_b_is_>=_than_Z_holds_
xl_<=_b
let b be Element of (subrelstr B); ::_thesis: ( b is_>=_than Z implies xl <= b )
reconsider b1 = b as Element of L by YELLOW_0:58;
assume A33: b is_>=_than Z ; ::_thesis: xl <= b
 b1 is_>=_than Z
proof
let c1 be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c1 in Z or c1 <= b1 )
assume A34: c1 in Z ; ::_thesis: c1 <= b1
then reconsider c = c1 as Element of (subrelstr B) ;
 c <= b by A33, A34, LATTICE3:def_9;
hence  c1 <= b1 by YELLOW_0:59; ::_thesis: verum
end;
then  "\/" (Z,L) <= b1 by A31, YELLOW_0:30;
hence  xl <= b by YELLOW_0:60; ::_thesis: verum
end;
A35: "\/" (Z,L) is_>=_than Z by A31, YELLOW_0:30;
 xl is_>=_than Z
proof
let b be Element of (subrelstr B); :: according to LATTICE3:def_9 ::_thesis: ( not b in Z or b <= xl )
reconsider b1 = b as Element of L by YELLOW_0:58;
assume  b in Z ; ::_thesis: b <= xl
then  b1 <= "\/" (Z,L) by A35, LATTICE3:def_9;
hence  b <= xl by YELLOW_0:60; ::_thesis: verum
end;
then  "\/" (Z,(subrelstr B)) = "\/" (Z,L) by A32, YELLOW_0:30;
then  "\/" (Y,L) <= srg by A21, YELLOW_0:32;
then A36: x1 <= srg by A7, A9, YELLOW_0:def_2;
 finsups (union X) c= downarrow (finsups (union X)) by WAYBEL_0:16;
hence  x in downarrow dfuX by A36, A30, WAYBEL_0:def_15; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_c=_union_((idsMap_(subrelstr_B))_.:_X)
let x be set ; ::_thesis: ( x in X implies x c= union ((idsMap (subrelstr B)) .: X) )
assume A37: x in X ; ::_thesis: x c= union ((idsMap (subrelstr B)) .: X)
then reconsider x1 = x as Ideal of (subrelstr B) by YELLOW_2:41;
consider x2 being Subset of L such that
A38: x1 = x2 and
A39: (idsMap (subrelstr B)) . x1 = downarrow x2 by Def11;
 x in the carrier of (InclPoset (Ids (subrelstr B))) by A37;
then  x1 in dom (idsMap (subrelstr B)) by FUNCT_2:def_1;
then A40: (idsMap (subrelstr B)) . x1 in (idsMap (subrelstr B)) .: X by A37, FUNCT_1:def_6;
thus  x c= union ((idsMap (subrelstr B)) .: X) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in union ((idsMap (subrelstr B)) .: X) )
assume A41: y in x ; ::_thesis: y in union ((idsMap (subrelstr B)) .: X)
 x c= downarrow x2 by A38, WAYBEL_0:16;
hence  y in union ((idsMap (subrelstr B)) .: X) by A39, A40, A41, TARSKI:def_4; ::_thesis: verum
end;
end;
then  union X c= union ((idsMap (subrelstr B)) .: X) by ZFMISC_1:76;
then A42: finsups unionX c= finsups (union ((idsMap (subrelstr B)) .: X)) by Th2;
 finsups (union X) c= finsups unionX by A3, A1, Th5;
then  finsups (union X) c= finsups (union ((idsMap (subrelstr B)) .: X)) by A42, XBOOLE_1:1;
then A43: downarrow fuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by YELLOW_3:6;
 downarrow (finsups (union X)) c= downarrow fuX by Th11;
then  dfuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by A43, XBOOLE_1:1;
then  downarrow dfuX c= downarrow (downarrow (finsups (union ((idsMap (subrelstr B)) .: X)))) by YELLOW_3:6;
then A44: downarrow dfuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by Th7;
thus  sup ((idsMap (subrelstr B)) .: X) = downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by Th6
.= downarrow dfuX by A5, A44, XBOOLE_0:def_10
.= (idsMap (subrelstr B)) . (sup X) by A4, Th6 ; ::_thesis: verum
end;
hence  idsMap (subrelstr B) preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
hence  idsMap (subrelstr B) is sups-preserving by WAYBEL_0:def_33; ::_thesis: verum
end;

theorem Th62: :: WAYBEL23:62
for L being non empty up-complete Poset
for S being non empty full SubRelStr of L holds supMap S = (SupMap L) * (idsMap S)
proof
let L be non empty up-complete Poset; ::_thesis: for S being non empty full SubRelStr of L holds supMap S = (SupMap L) * (idsMap S)
let S be non empty full SubRelStr of L; ::_thesis: supMap S = (SupMap L) * (idsMap S)
A1: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(supMap_S)_implies_(_x_in_dom_(idsMap_S)_&_(idsMap_S)_._x_in_dom_(SupMap_L)_)_)_&_(_x_in_dom_(idsMap_S)_&_(idsMap_S)_._x_in_dom_(SupMap_L)_implies_x_in_dom_(supMap_S)_)_)
let x be set ; ::_thesis: ( ( x in dom (supMap S) implies ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) ) ) & ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) implies x in dom (supMap S) ) )
thus  ( x in dom (supMap S) implies ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) ) ) ::_thesis: ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) implies x in dom (supMap S) )
proof
assume  x in dom (supMap S) ; ::_thesis: ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) )
then  x is Ideal of S by Th52;
hence  x in dom (idsMap S) by Th54; ::_thesis: (idsMap S) . x in dom (SupMap L)
then  (idsMap S) . x in rng (idsMap S) by FUNCT_1:def_3;
then  (idsMap S) . x is Ideal of L by Th55;
hence  (idsMap S) . x in dom (SupMap L) by YELLOW_2:50; ::_thesis: verum
end;
thus  ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) implies x in dom (supMap S) ) ::_thesis: verum
proof
assume that
A2: x in dom (idsMap S) and
 (idsMap S) . x in dom (SupMap L) ; ::_thesis: x in dom (supMap S)
 x is Ideal of S by A2, Th54;
hence  x in dom (supMap S) by Th52; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_(supMap_S)_holds_
(supMap_S)_._x_=_(SupMap_L)_._((idsMap_S)_._x)
let x be set ; ::_thesis: ( x in dom (supMap S) implies (supMap S) . x = (SupMap L) . ((idsMap S) . x) )
assume  x in dom (supMap S) ; ::_thesis: (supMap S) . x = (SupMap L) . ((idsMap S) . x)
then reconsider I = x as Ideal of S by Th52;
consider J being Subset of L such that
A3: I = J and
A4: (idsMap S) . I = downarrow J by Def11;
reconsider J = J as non empty directed Subset of L by A3, YELLOW_2:7;
A5: ex_sup_of J,L by WAYBEL_0:75;
thus (supMap S) . x = "\/" (I,L) by Def10
.= sup (downarrow J) by A3, A5, WAYBEL_0:33
.= (SupMap L) . ((idsMap S) . x) by A4, YELLOW_2:def_3 ; ::_thesis: verum
end;
hence  supMap S = (SupMap L) * (idsMap S) by A1, FUNCT_1:10; ::_thesis: verum
end;

theorem Th63: :: WAYBEL23:63
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois
let B be with_bottom CLbasis of L; ::_thesis: [(supMap (subrelstr B)),(baseMap B)] is Galois
now__::_thesis:_for_x_being_Element_of_L
for_y_being_Element_of_(InclPoset_(Ids_(subrelstr_B)))_holds_
(_(_x_<=_(supMap_(subrelstr_B))_._y_implies_(baseMap_B)_._x_<=_y_)_&_(_(baseMap_B)_._x_<=_y_implies_x_<=_(supMap_(subrelstr_B))_._y_)_)
let x be Element of L; ::_thesis: for y being Element of (InclPoset (Ids (subrelstr B))) holds
( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )
let y be Element of (InclPoset (Ids (subrelstr B))); ::_thesis: ( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )
reconsider I = y as Ideal of (subrelstr B) by YELLOW_2:41;
reconsider J = I as non empty directed Subset of L by YELLOW_2:7;
A1: ex_sup_of (waybelow x) /\ B,L by YELLOW_0:17;
thus  ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) ::_thesis: ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y )
proof
A2: (downarrow J) /\ B c= J
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (downarrow J) /\ B or z in J )
assume A3: z in (downarrow J) /\ B ; ::_thesis: z in J
then reconsider z1 = z as Element of L ;
 z in B by A3, XBOOLE_0:def_4;
then reconsider z2 = z as Element of (subrelstr B) by YELLOW_0:def_15;
 z in downarrow J by A3, XBOOLE_0:def_4;
then consider v1 being Element of L such that
A4: v1 >= z1 and
A5: v1 in J by WAYBEL_0:def_15;
reconsider v2 = v1 as Element of (subrelstr B) by A5;
 z2 <= v2 by A4, YELLOW_0:60;
hence  z in J by A5, WAYBEL_0:def_19; ::_thesis: verum
end;
assume  x <= (supMap (subrelstr B)) . y ; ::_thesis: (baseMap B) . x <= y
then  x <= "\/" (I,L) by Def10;
then A6: x <= sup (downarrow J) by WAYBEL_0:33, YELLOW_0:17;
 waybelow x c= downarrow J
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in waybelow x or z in downarrow J )
assume A7: z in waybelow x ; ::_thesis: z in downarrow J
then reconsider z1 = z as Element of L ;
 z1 << x by A7, WAYBEL_3:7;
hence  z in downarrow J by A6, WAYBEL_3:20; ::_thesis: verum
end;
then  (waybelow x) /\ B c= (downarrow J) /\ B by XBOOLE_1:26;
then  (waybelow x) /\ B c= y by A2, XBOOLE_1:1;
then  (baseMap B) . x c= y by Def12;
hence  (baseMap B) . x <= y by YELLOW_1:3; ::_thesis: verum
end;
A8: ex_sup_of J,L by YELLOW_0:17;
thus  ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) ::_thesis: verum
proof
assume  (baseMap B) . x <= y ; ::_thesis: x <= (supMap (subrelstr B)) . y
then  (baseMap B) . x c= y by YELLOW_1:3;
then  (waybelow x) /\ B c= y by Def12;
then  sup ((waybelow x) /\ B) <= sup J by A8, A1, YELLOW_0:34;
then  x <= "\/" (I,L) by Def7;
hence  x <= (supMap (subrelstr B)) . y by Def10; ::_thesis: verum
end;
end;
hence  [(supMap (subrelstr B)),(baseMap B)] is Galois by WAYBEL_1:8; ::_thesis: verum
end;

theorem Th64: :: WAYBEL23:64
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )
let B be with_bottom CLbasis of L; ::_thesis: ( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )
 [(supMap (subrelstr B)),(baseMap B)] is Galois by Th63;
hence  ( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint ) by WAYBEL_1:9; ::_thesis: verum
end;

theorem Th65: :: WAYBEL23:65
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds rng (supMap (subrelstr B)) = the carrier of L
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds rng (supMap (subrelstr B)) = the carrier of L
let B be with_bottom CLbasis of L; ::_thesis: rng (supMap (subrelstr B)) = the carrier of L
A1: Bottom L in B by Def8;
thus  rng (supMap (subrelstr B)) = the carrier of L ::_thesis: verum
proof
thus  rng (supMap (subrelstr B)) c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= rng (supMap (subrelstr B))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in rng (supMap (subrelstr B)) )
assume  x in the carrier of L ; ::_thesis: x in rng (supMap (subrelstr B))
then reconsider x1 = x as Element of L ;
set z = (waybelow x1) /\ B;
 (waybelow x1) /\ B is Subset of B by XBOOLE_1:17;
then reconsider z = (waybelow x1) /\ B as Subset of (subrelstr B) by YELLOW_0:def_15;
A2: now__::_thesis:_for_a,_b_being_Element_of_(subrelstr_B)_st_a_in_z_&_b_<=_a_holds_
b_in_z
let a, b be Element of (subrelstr B); ::_thesis: ( a in z & b <= a implies b in z )
reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;
assume that
A3: a in z and
A4: b <= a ; ::_thesis: b in z
 a in waybelow x1 by A3, XBOOLE_0:def_4;
then A5: a1 << x1 by WAYBEL_3:7;
 b1 <= a1 by A4, YELLOW_0:59;
then  b1 << x1 by A5, WAYBEL_3:2;
then A6: b in waybelow x1 by WAYBEL_3:7;
 b in the carrier of (subrelstr B) ;
then  b in B by YELLOW_0:def_15;
hence  b in z by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
 Bottom L << x1 by WAYBEL_3:4;
then A7: Bottom L in waybelow x1 by WAYBEL_3:7;
 (waybelow x1) /\ B is join-closed by Th33;
then reconsider z = z as Ideal of (subrelstr B) by A1, A7, A2, WAYBEL10:23, WAYBEL_0:def_19, XBOOLE_0:def_4;
 z in  {  X where X is Ideal of (subrelstr B) : verum  }  ;
then  z in Ids (subrelstr B) by WAYBEL_0:def_23;
then A8: z in dom (supMap (subrelstr B)) by Th51;
x = "\/" (z,L) by Def7
.= (supMap (subrelstr B)) . z by Def10 ;
hence  x in rng (supMap (subrelstr B)) by A8, FUNCT_1:def_3; ::_thesis: verum
end;
end;

theorem Th66: :: WAYBEL23:66
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )
let B be with_bottom CLbasis of L; ::_thesis: ( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )
A1: SupMap L is sups-preserving by WAYBEL13:33;
thus  supMap (subrelstr B) is infs-preserving by Th64, WAYBEL_1:12; ::_thesis: supMap (subrelstr B) is sups-preserving
A2: supMap (subrelstr B) = (SupMap L) * (idsMap (subrelstr B)) by Th62;
 idsMap (subrelstr B) is sups-preserving by Th61;
hence  supMap (subrelstr B) is sups-preserving by A2, A1, WAYBEL20:27; ::_thesis: verum
end;

theorem :: WAYBEL23:67
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds baseMap B is sups-preserving by Th64, WAYBEL_1:13;

registration
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster supMap (subrelstr B) ->  infs-preserving sups-preserving ;
coherence
 ( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving ) by Th66;
cluster baseMap B ->  sups-preserving ;
coherence
 baseMap B is sups-preserving by Th64, WAYBEL_1:13;
end;

theorem Th68: :: WAYBEL23:68
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) =  {  (downarrow b) where b is Element of (subrelstr B) : verum  }
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) =  {  (downarrow b) where b is Element of (subrelstr B) : verum  }
let B be with_bottom CLbasis of L; ::_thesis: the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) =  {  (downarrow b) where b is Element of (subrelstr B) : verum  }
thus  the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) c=  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  c= the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B))))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) or x in  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  )
assume A1: x in the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) ; ::_thesis: x in  {  (downarrow b) where b is Element of (subrelstr B) : verum  }
 the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) c= the carrier of (InclPoset (Ids (subrelstr B))) by YELLOW_0:def_13;
then reconsider x1 = x as Element of (InclPoset (Ids (subrelstr B))) by A1;
 x1 is compact by A1, WAYBEL_8:def_1;
then  ex b being Element of (subrelstr B) st x1 = downarrow b by WAYBEL13:12;
hence  x in  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  ; ::_thesis: verum
end;
thus   {  (downarrow b) where b is Element of (subrelstr B) : verum  }  c= the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  or x in the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) )
assume  x in  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  ; ::_thesis: x in the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B))))
then A2: ex b being Element of (subrelstr B) st x = downarrow b ;
then reconsider x1 = x as Element of (InclPoset (Ids (subrelstr B))) by YELLOW_2:41;
 x1 is compact by A2, WAYBEL13:12;
hence  x in the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) by WAYBEL_8:def_1; ::_thesis: verum
end;
end;

theorem :: WAYBEL23:69
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic
let B be with_bottom CLbasis of L; ::_thesis: CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic
deffunc H1( Element of (subrelstr B)) ->  Element of K32( the carrier of (subrelstr B)) = downarrow $1;
A1: for x being Element of (subrelstr B) holds H1(x) is Element of (CompactSublatt (InclPoset (Ids (subrelstr B))))
proof
let x be Element of (subrelstr B); ::_thesis: H1(x) is Element of (CompactSublatt (InclPoset (Ids (subrelstr B))))
 downarrow x in  {  (downarrow b) where b is Element of (subrelstr B) : verum  }  ;
hence  H1(x) is Element of (CompactSublatt (InclPoset (Ids (subrelstr B)))) by Th68; ::_thesis: verum
end;
consider f being Function of (subrelstr B),(CompactSublatt (InclPoset (Ids (subrelstr B)))) such that
A2: for x being Element of (subrelstr B) holds f . x = H1(x) from FUNCT_2:sch_9(A1);
 f is isomorphic by A2, WAYBEL13:13;
then  subrelstr B, CompactSublatt (InclPoset (Ids (subrelstr B))) are_isomorphic by WAYBEL_1:def_8;
hence  CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic by WAYBEL_1:6; ::_thesis: verum
end;

Lm4:  for L being lower-bounded continuous LATTICE st L is algebraic holds
( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: ( L is algebraic implies ( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) ) )
assume  L is algebraic ; ::_thesis: ( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )
hence  the carrier of (CompactSublatt L) is with_bottom CLbasis of L by Th44; ::_thesis: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B
let B be with_bottom CLbasis of L; ::_thesis: the carrier of (CompactSublatt L) c= B
 Bottom L in B by Def8;
hence  the carrier of (CompactSublatt L) c= B by Th48; ::_thesis: verum
end;

theorem Th70: :: WAYBEL23:70
for L being lower-bounded continuous LATTICE
for B being with_bottom CLbasis of L st ( for B1 being with_bottom CLbasis of L holds B c= B1 ) holds
for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for B being with_bottom CLbasis of L st ( for B1 being with_bottom CLbasis of L holds B c= B1 ) holds
for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B
let B be with_bottom CLbasis of L; ::_thesis: ( ( for B1 being with_bottom CLbasis of L holds B c= B1 ) implies for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B )
assume A1: for B1 being with_bottom CLbasis of L holds B c= B1 ; ::_thesis: for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B
let J be Element of (InclPoset (Ids (subrelstr B))); ::_thesis: J = (waybelow ("\/" (J,L))) /\ B
reconsider J1 = J as Ideal of (subrelstr B) by YELLOW_2:41;
reconsider J2 = J1 as non empty directed Subset of L by YELLOW_2:7;
set x = "\/" (J,L);
set C = (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B);
A2: (waybelow ("\/" (J,L))) /\ B c= B by XBOOLE_1:17;
 B \ J2 c= B by XBOOLE_1:36;
then A3: (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) c= B by A2, XBOOLE_1:8;
A4: now__::_thesis:_for_y_being_Element_of_L_holds_y_=_sup_((waybelow_y)_/\_((B_\_J2)_\/_((waybelow_("\/"_(J,L)))_/\_B)))
let y be Element of L; ::_thesis: b1 = sup ((waybelow b1) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
percases ( not y <= "\/" (J,L) or y <= "\/" (J,L) ) ;
suppose not y <= "\/" (J,L) ; ::_thesis: b1 = sup ((waybelow b1) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
then consider u being Element of L such that
A5: u in B and
A6: not u <= "\/" (J,L) and
A7: u << y by Th46;
A8: now__::_thesis:_for_b_being_Element_of_L_st_b_is_>=_than_(waybelow_y)_/\_((B_\_J2)_\/_((waybelow_("\/"_(J,L)))_/\_B))_holds_
sup_((waybelow_y)_/\_B)_<=_b
let b be Element of L; ::_thesis: ( b is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) implies sup ((waybelow y) /\ B) <= b )
assume A9: b is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) ; ::_thesis: sup ((waybelow y) /\ B) <= b
 b is_>=_than (waybelow y) /\ B
proof
let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in (waybelow y) /\ B or c <= b )
 u <= c "\/" u by YELLOW_0:22;
then A10: not c "\/" u <= "\/" (J,L) by A6, YELLOW_0:def_2;
assume A11: c in (waybelow y) /\ B ; ::_thesis: c <= b
then  c in B by XBOOLE_0:def_4;
then  sup {c,u} in B by A5, Th18;
then A12: c "\/" u in B by YELLOW_0:41;
 J is_<=_than "\/" (J,L) by YELLOW_0:32;
then  not c "\/" u in J by A10, LATTICE3:def_9;
then  c "\/" u in B \ J by A12, XBOOLE_0:def_5;
then A13: c "\/" u in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_3;
 c in waybelow y by A11, XBOOLE_0:def_4;
then  c << y by WAYBEL_3:7;
then  c "\/" u << y by A7, WAYBEL_3:3;
then  c "\/" u in waybelow y by WAYBEL_3:7;
then  c "\/" u in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A13, XBOOLE_0:def_4;
then A14: c "\/" u <= b by A9, LATTICE3:def_9;
 c <= c "\/" u by YELLOW_0:22;
hence  c <= b by A14, YELLOW_0:def_2; ::_thesis: verum
end;
hence  sup ((waybelow y) /\ B) <= b by YELLOW_0:32; ::_thesis: verum
end;
A15: (waybelow y) /\ B is_<=_than sup ((waybelow y) /\ B) by YELLOW_0:32;
 sup ((waybelow y) /\ B) is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) or b <= sup ((waybelow y) /\ B) )
assume A16: b in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) ; ::_thesis: b <= sup ((waybelow y) /\ B)
then A17: b in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_4;
 b in waybelow y by A16, XBOOLE_0:def_4;
then  b in (waybelow y) /\ B by A3, A17, XBOOLE_0:def_4;
hence  b <= sup ((waybelow y) /\ B) by A15, LATTICE3:def_9; ::_thesis: verum
end;
then  sup ((waybelow y) /\ B) = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by A8, YELLOW_0:32;
hence  y = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by Def7; ::_thesis: verum
end;
supposeA18: y <= "\/" (J,L) ; ::_thesis: b1 = sup ((waybelow b1) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
A19: (waybelow y) /\ B c= (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (waybelow y) /\ B or a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) )
assume A20: a in (waybelow y) /\ B ; ::_thesis: a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
then reconsider a1 = a as Element of L ;
A21: a in waybelow y by A20, XBOOLE_0:def_4;
then  a1 << y by WAYBEL_3:7;
then  a1 << "\/" (J,L) by A18, WAYBEL_3:2;
then A22: a1 in waybelow ("\/" (J,L)) by WAYBEL_3:7;
 a in B by A20, XBOOLE_0:def_4;
then  a in (waybelow ("\/" (J,L))) /\ B by A22, XBOOLE_0:def_4;
then  a in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_3;
hence  a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A21, XBOOLE_0:def_4; ::_thesis: verum
end;
 (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) c= (waybelow y) /\ B by A3, XBOOLE_1:26;
then  (waybelow y) /\ B = (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A19, XBOOLE_0:def_10;
hence  y = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by Def7; ::_thesis: verum
end;
end;
end;
A23: subrelstr B is join-inheriting by Def2;
 subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) is join-inheriting
proof
let a, b be Element of L; :: according to YELLOW_0:def_17 ::_thesis: ( not a in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) or not b in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) or not ex_sup_of {a,b},L or "\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) )
assume that
A24: a in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) and
A25: b in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) and
A26: ex_sup_of {a,b},L ; ::_thesis: "\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
A27: b in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by A25, YELLOW_0:def_15;
A28: a in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by A24, YELLOW_0:def_15;
then A29: sup {a,b} in B by A3, A26, A27, Th16;
reconsider a1 = a, b1 = b as Element of (subrelstr B) by A3, A28, A27, YELLOW_0:def_15;
A30: a1 <= a1 "\/" b1 by YELLOW_0:22;
A31: b1 <= a1 "\/" b1 by YELLOW_0:22;
now__::_thesis:_sup_{a,b}_in_(B_\_J2)_\/_((waybelow_("\/"_(J,L)))_/\_B)
percases ( ( a in B \ J & b in B \ J ) or ( a in B \ J & b in (waybelow ("\/" (J,L))) /\ B ) or ( a in (waybelow ("\/" (J,L))) /\ B & b in B \ J ) or ( a in (waybelow ("\/" (J,L))) /\ B & b in (waybelow ("\/" (J,L))) /\ B ) ) by A28, A27, XBOOLE_0:def_3;
suppose ( a in B \ J & b in B \ J ) ; ::_thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then A32: not a in J by XBOOLE_0:def_5;
 not a "\/" b in J
proof
assume  a "\/" b in J ; ::_thesis: contradiction
then  a1 "\/" b1 in J1 by A23, YELLOW_0:70;
hence  contradiction by A30, A32, WAYBEL_0:def_19; ::_thesis: verum
end;
then  not sup {a,b} in J by YELLOW_0:41;
then  sup {a,b} in B \ J by A29, XBOOLE_0:def_5;
hence  sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( a in B \ J & b in (waybelow ("\/" (J,L))) /\ B ) ; ::_thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then A33: not a in J by XBOOLE_0:def_5;
 not a "\/" b in J
proof
assume  a "\/" b in J ; ::_thesis: contradiction
then  a1 "\/" b1 in J1 by A23, YELLOW_0:70;
hence  contradiction by A30, A33, WAYBEL_0:def_19; ::_thesis: verum
end;
then  not sup {a,b} in J by YELLOW_0:41;
then  sup {a,b} in B \ J by A29, XBOOLE_0:def_5;
hence  sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( a in (waybelow ("\/" (J,L))) /\ B & b in B \ J ) ; ::_thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then A34: not b in J by XBOOLE_0:def_5;
 not a "\/" b in J
proof
assume  a "\/" b in J ; ::_thesis: contradiction
then  a1 "\/" b1 in J1 by A23, YELLOW_0:70;
hence  contradiction by A31, A34, WAYBEL_0:def_19; ::_thesis: verum
end;
then  not sup {a,b} in J by YELLOW_0:41;
then  sup {a,b} in B \ J by A29, XBOOLE_0:def_5;
hence  sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA35: ( a in (waybelow ("\/" (J,L))) /\ B & b in (waybelow ("\/" (J,L))) /\ B ) ; ::_thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then  b in waybelow ("\/" (J,L)) by XBOOLE_0:def_4;
then A36: b << "\/" (J,L) by WAYBEL_3:7;
 a in waybelow ("\/" (J,L)) by A35, XBOOLE_0:def_4;
then  a << "\/" (J,L) by WAYBEL_3:7;
then  a "\/" b << "\/" (J,L) by A36, WAYBEL_3:3;
then  a "\/" b in waybelow ("\/" (J,L)) by WAYBEL_3:7;
then  sup {a,b} in waybelow ("\/" (J,L)) by YELLOW_0:41;
then  sup {a,b} in (waybelow ("\/" (J,L))) /\ B by A29, XBOOLE_0:def_4;
hence  sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  "\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by YELLOW_0:def_15; ::_thesis: verum
end;
then A37: (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) is join-closed by Def2;
 Bottom L << "\/" (J,L) by WAYBEL_3:4;
then A38: Bottom L in waybelow ("\/" (J,L)) by WAYBEL_3:7;
reconsider C = (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) as CLbasis of L by A37, A4, Def7;
 Bottom L in B by Def8;
then  Bottom L in (waybelow ("\/" (J,L))) /\ B by A38, XBOOLE_0:def_4;
then  Bottom L in C by XBOOLE_0:def_3;
then  C is with_bottom by Def8;
then  B c= C by A1;
then A39: B = C by A3, XBOOLE_0:def_10;
A40: J c= (waybelow ("\/" (J,L))) /\ B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in J or a in (waybelow ("\/" (J,L))) /\ B )
assume A41: a in J ; ::_thesis: a in (waybelow ("\/" (J,L))) /\ B
then  a in J1 ;
then  a in the carrier of (subrelstr B) ;
then A42: a in C by A39, YELLOW_0:def_15;
 not a in B \ J2 by A41, XBOOLE_0:def_5;
hence  a in (waybelow ("\/" (J,L))) /\ B by A42, XBOOLE_0:def_3; ::_thesis: verum
end;
 (waybelow ("\/" (J,L))) /\ B c= J
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (waybelow ("\/" (J,L))) /\ B or a in J )
assume A43: a in (waybelow ("\/" (J,L))) /\ B ; ::_thesis: a in J
then reconsider a1 = a as Element of L ;
 a in B by A43, XBOOLE_0:def_4;
then reconsider a2 = a as Element of (subrelstr B) by YELLOW_0:def_15;
 a in waybelow ("\/" (J,L)) by A43, XBOOLE_0:def_4;
then  a1 << "\/" (J,L) by WAYBEL_3:7;
then consider d1 being Element of L such that
A44: d1 in J2 and
A45: a1 <= d1 by WAYBEL_3:def_1;
reconsider d2 = d1 as Element of (subrelstr B) by A44;
 a2 <= d2 by A45, YELLOW_0:60;
hence  a in J by A44, WAYBEL_0:def_19; ::_thesis: verum
end;
hence  J = (waybelow ("\/" (J,L))) /\ B by A40, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm5:  for L being lower-bounded continuous LATTICE st ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 holds
L is algebraic
proof
let L be lower-bounded continuous LATTICE; ::_thesis: ( ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )
given B being with_bottom CLbasis of L such that A1: for B1 being with_bottom CLbasis of L holds B c= B1 ; ::_thesis: L is algebraic
A2: for x, y being Element of (InclPoset (Ids (subrelstr B))) holds
( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )
proof
let x, y be Element of (InclPoset (Ids (subrelstr B))); ::_thesis: ( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )
thus  ( x <= y implies (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ) by WAYBEL_1:def_2; ::_thesis: ( (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y implies x <= y )
reconsider x1 = x, y1 = y as Ideal of (subrelstr B) by YELLOW_2:41;
assume A3: (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ; ::_thesis: x <= y
A4: (supMap (subrelstr B)) . y1 = "\/" (y1,L) by Def10;
 (supMap (subrelstr B)) . x1 = "\/" (x1,L) by Def10;
then  waybelow ("\/" (x1,L)) c= waybelow ("\/" (y1,L)) by A4, A3, WAYBEL_3:25;
then A5: (waybelow ("\/" (x1,L))) /\ B c= (waybelow ("\/" (y1,L))) /\ B by XBOOLE_1:26;
A6: y = (waybelow ("\/" (y,L))) /\ B by A1, Th70;
 x = (waybelow ("\/" (x,L))) /\ B by A1, Th70;
hence  x <= y by A6, A5, YELLOW_1:3; ::_thesis: verum
end;
 the carrier of (InclPoset (Ids (subrelstr B))) c= rng (baseMap B)
proof
let J be set ; :: according to TARSKI:def_3 ::_thesis: ( not J in the carrier of (InclPoset (Ids (subrelstr B))) or J in rng (baseMap B) )
set x = "\/" (J,L);
assume  J in the carrier of (InclPoset (Ids (subrelstr B))) ; ::_thesis: J in rng (baseMap B)
then  J = (waybelow ("\/" (J,L))) /\ B by A1, Th70;
then A7: J = (baseMap B) . ("\/" (J,L)) by Def12;
 dom (baseMap B) = the carrier of L by FUNCT_2:def_1;
hence  J in rng (baseMap B) by A7, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng (baseMap B) = the carrier of (InclPoset (Ids (subrelstr B))) by XBOOLE_0:def_10;
then A8: baseMap B is onto by FUNCT_2:def_3;
 [(supMap (subrelstr B)),(baseMap B)] is Galois by Th63;
then A9: supMap (subrelstr B) is V13() by A8, WAYBEL_1:27;
 rng (supMap (subrelstr B)) = the carrier of L by Th65;
then  supMap (subrelstr B) is isomorphic by A9, A2, WAYBEL_0:66;
then A10: InclPoset (Ids (subrelstr B)),L are_isomorphic by WAYBEL_1:def_8;
 ( InclPoset (Ids (subrelstr B)) is lower-bounded & InclPoset (Ids (subrelstr B)) is algebraic ) by WAYBEL13:10;
hence  L is algebraic by A10, WAYBEL13:32; ::_thesis: verum
end;

theorem :: WAYBEL23:71
for L being lower-bounded continuous LATTICE holds
( L is algebraic iff ( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) ) ) by Lm4, Lm5;

theorem :: WAYBEL23:72
for L being lower-bounded continuous LATTICE holds
( L is algebraic iff ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: ( L is algebraic iff ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 )
thus  ( L is algebraic implies ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 ) ::_thesis: ( ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )
proof
assume A1: L is algebraic ; ::_thesis: ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1
then A2: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B by Lm4;
 the carrier of (CompactSublatt L) is with_bottom CLbasis of L by A1, Lm4;
hence  ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 by A2; ::_thesis: verum
end;
thus  ( ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic ) by Lm5; ::_thesis: verum
end;

theorem :: WAYBEL23:73
for T being TopStruct
for b being Basis of T holds weight T c= card b
proof
let T be TopStruct ; ::_thesis: for b being Basis of T holds weight T c= card b
let b be Basis of T; ::_thesis: weight T c= card b
 card b in  {  (card B1) where B1 is Basis of T : verum  }  ;
hence  weight T c= card b by SETFAM_1:3; ::_thesis: verum
end;

theorem :: WAYBEL23:74
for T being TopStruct ex b being Basis of T st card b = weight T
proof
let T be TopStruct ; ::_thesis: ex b being Basis of T st card b = weight T
defpred S1[ Ordinal] means $1 in  {  (card b) where b is Basis of T : verum  }  ;
set X =  {  (card b1) where b1 is Basis of T : verum  }  ;
A1: ex A being Ordinal st S1[A]
proof
take  card the topology of T ; ::_thesis: S1[ card the topology of T]
 the topology of T is Basis of T by CANTOR_1:2;
hence  S1[ card the topology of T] ; ::_thesis: verum
end;
consider A being Ordinal such that
A2: S1[A] and
A3: for C being Ordinal st S1[C] holds
A c= C from ORDINAL1:sch_1(A1);
consider b being Basis of T such that
A4: A = card b by A2;
A5: now__::_thesis:_for_x_being_set_holds_
(_(_(_for_y_being_set_st_y_in__{__(card_b1)_where_b1_is_Basis_of_T_:_verum__}__holds_
x_in_y_)_implies_x_in_A_)_&_(_x_in_A_implies_for_y_being_set_st_y_in__{__(card_b1)_where_b1_is_Basis_of_T_:_verum__}__holds_
x_in_y_)_)
let x be set ; ::_thesis: ( ( ( for y being set st y in  {  (card b1) where b1 is Basis of T : verum  }  holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in  {  (card b1) where b1 is Basis of T : verum  }  holds
x in y ) )
thus  ( ( for y being set st y in  {  (card b1) where b1 is Basis of T : verum  }  holds
x in y ) implies x in A ) by A2; ::_thesis: ( x in A implies for y being set st y in  {  (card b1) where b1 is Basis of T : verum  }  holds
x in y )
assume A6: x in A ; ::_thesis: for y being set st y in  {  (card b1) where b1 is Basis of T : verum  }  holds
x in y
let y be set ; ::_thesis: ( y in  {  (card b1) where b1 is Basis of T : verum  }  implies x in y )
assume A7: y in  {  (card b1) where b1 is Basis of T : verum  }  ; ::_thesis: x in y
then  ex B2 being Basis of T st y = card B2 ;
then reconsider y1 = y as Cardinal ;
 A c= y1 by A3, A7;
hence  x in y by A6; ::_thesis: verum
end;
take  b ; ::_thesis: card b = weight T
 the topology of T is Basis of T by CANTOR_1:2;
then  card the topology of T in  {  (card b1) where b1 is Basis of T : verum  }  ;
hence  card b = weight T by A4, A5, SETFAM_1:def_1; ::_thesis: verum
end;