:: WAYBEL16 semantic presentation

begin

theorem Th1: :: WAYBEL16:1
for L being sup-Semilattice
for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y
proof
let L be sup-Semilattice; ::_thesis: for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y
let x, y be Element of L; ::_thesis: "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y
 (uparrow x) /\ (uparrow y) = uparrow (x "\/" y) by WAYBEL14:4;
hence  "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y by WAYBEL_0:39; ::_thesis: verum
end;

theorem :: WAYBEL16:2
for L being Semilattice
for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
proof
let L be Semilattice; ::_thesis: for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
let x, y be Element of L; ::_thesis: "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
 (downarrow x) /\ (downarrow y) = downarrow (x "/\" y) by WAYBEL14:3;
hence  "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y by WAYBEL_0:34; ::_thesis: verum
end;

theorem Th3: :: WAYBEL16:3
for L being non empty RelStr
for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds
(uparrow x) \ {x} = (uparrow x) /\ (uparrow y)
proof
let L be non empty RelStr ; ::_thesis: for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds
(uparrow x) \ {x} = (uparrow x) /\ (uparrow y)
let x, y be Element of L; ::_thesis: ( x is_maximal_in the carrier of L \ (uparrow y) implies (uparrow x) \ {x} = (uparrow x) /\ (uparrow y) )
assume A1: x is_maximal_in the carrier of L \ (uparrow y) ; ::_thesis: (uparrow x) \ {x} = (uparrow x) /\ (uparrow y)
then  x in the carrier of L \ (uparrow y) by WAYBEL_4:55;
then  not x in uparrow y by XBOOLE_0:def_5;
then A2: not y <= x by WAYBEL_0:18;
thus  (uparrow x) \ {x} c= (uparrow x) /\ (uparrow y) :: according to XBOOLE_0:def_10 ::_thesis: (uparrow x) /\ (uparrow y) c= (uparrow x) \ {x}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (uparrow x) \ {x} or a in (uparrow x) /\ (uparrow y) )
assume A3: a in (uparrow x) \ {x} ; ::_thesis: a in (uparrow x) /\ (uparrow y)
then reconsider a1 = a as Element of L ;
 not a in {x} by A3, XBOOLE_0:def_5;
then A4: a1 <> x by TARSKI:def_1;
A5: a in uparrow x by A3, XBOOLE_0:def_5;
then  x <= a1 by WAYBEL_0:18;
then  x < a1 by A4, ORDERS_2:def_6;
then  not a1 in the carrier of L \ (uparrow y) by A1, WAYBEL_4:55;
then  a in uparrow y by XBOOLE_0:def_5;
hence  a in (uparrow x) /\ (uparrow y) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (uparrow x) /\ (uparrow y) or a in (uparrow x) \ {x} )
assume A6: a in (uparrow x) /\ (uparrow y) ; ::_thesis: a in (uparrow x) \ {x}
then A7: a in uparrow x by XBOOLE_0:def_4;
reconsider a1 = a as Element of L by A6;
 a in uparrow y by A6, XBOOLE_0:def_4;
then  y <= a1 by WAYBEL_0:18;
then  not a in {x} by A2, TARSKI:def_1;
hence  a in (uparrow x) \ {x} by A7, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: WAYBEL16:4
for L being non empty RelStr
for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds
(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)
proof
let L be non empty RelStr ; ::_thesis: for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds
(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)
let x, y be Element of L; ::_thesis: ( x is_minimal_in the carrier of L \ (downarrow y) implies (downarrow x) \ {x} = (downarrow x) /\ (downarrow y) )
assume A1: x is_minimal_in the carrier of L \ (downarrow y) ; ::_thesis: (downarrow x) \ {x} = (downarrow x) /\ (downarrow y)
then  x in the carrier of L \ (downarrow y) by WAYBEL_4:56;
then  not x in downarrow y by XBOOLE_0:def_5;
then A2: not x <= y by WAYBEL_0:17;
thus  (downarrow x) \ {x} c= (downarrow x) /\ (downarrow y) :: according to XBOOLE_0:def_10 ::_thesis: (downarrow x) /\ (downarrow y) c= (downarrow x) \ {x}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (downarrow x) \ {x} or a in (downarrow x) /\ (downarrow y) )
assume A3: a in (downarrow x) \ {x} ; ::_thesis: a in (downarrow x) /\ (downarrow y)
then reconsider a1 = a as Element of L ;
 not a in {x} by A3, XBOOLE_0:def_5;
then A4: a1 <> x by TARSKI:def_1;
A5: a in downarrow x by A3, XBOOLE_0:def_5;
then  a1 <= x by WAYBEL_0:17;
then  a1 < x by A4, ORDERS_2:def_6;
then  not a1 in the carrier of L \ (downarrow y) by A1, WAYBEL_4:56;
then  a in downarrow y by XBOOLE_0:def_5;
hence  a in (downarrow x) /\ (downarrow y) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (downarrow x) /\ (downarrow y) or a in (downarrow x) \ {x} )
assume A6: a in (downarrow x) /\ (downarrow y) ; ::_thesis: a in (downarrow x) \ {x}
then A7: a in downarrow x by XBOOLE_0:def_4;
reconsider a1 = a as Element of L by A6;
 a in downarrow y by A6, XBOOLE_0:def_4;
then  a1 <= y by WAYBEL_0:17;
then  not a in {x} by A2, TARSKI:def_1;
hence  a in (downarrow x) \ {x} by A7, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th5: :: WAYBEL16:5
for L being with_suprema Poset
for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9
proof
let L be with_suprema Poset; ::_thesis: for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9
let X, Y be Subset of L; ::_thesis: for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9
let X9, Y9 be Subset of (L opp); ::_thesis: ( X = X9 & Y = Y9 implies X "\/" Y = X9 "/\" Y9 )
assume A1: ( X = X9 & Y = Y9 ) ; ::_thesis: X "\/" Y = X9 "/\" Y9
thus  X "\/" Y c= X9 "/\" Y9 :: according to XBOOLE_0:def_10 ::_thesis: X9 "/\" Y9 c= X "\/" Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "\/" Y or a in X9 "/\" Y9 )
assume  a in X "\/" Y ; ::_thesis: a in X9 "/\" Y9
then  a in  {  (p "\/" q) where p, q is Element of L : ( p in X & q in Y )  }  by YELLOW_4:def_3;
then consider x, y being Element of L such that
A2: a = x "\/" y and
A3: ( x in X & y in Y ) ;
A4: a = (x ~) "/\" (y ~) by A2, YELLOW_7:23;
 ( x ~ in X9 & y ~ in Y9 ) by A1, A3, LATTICE3:def_6;
then  a in  {  (p "/\" q) where p, q is Element of (L opp) : ( p in X9 & q in Y9 )  }  by A4;
hence  a in X9 "/\" Y9 by YELLOW_4:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X9 "/\" Y9 or a in X "\/" Y )
assume  a in X9 "/\" Y9 ; ::_thesis: a in X "\/" Y
then  a in  {  (p "/\" q) where p, q is Element of (L opp) : ( p in X9 & q in Y9 )  }  by YELLOW_4:def_4;
then consider x, y being Element of (L opp) such that
A5: a = x "/\" y and
A6: ( x in X9 & y in Y9 ) ;
A7: a = (~ x) "\/" (~ y) by A5, YELLOW_7:24;
 ( ~ x in X & ~ y in Y ) by A1, A6, LATTICE3:def_7;
then  a in  {  (p "\/" q) where p, q is Element of L : ( p in X & q in Y )  }  by A7;
hence  a in X "\/" Y by YELLOW_4:def_3; ::_thesis: verum
end;

theorem :: WAYBEL16:6
for L being with_infima Poset
for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "/\" Y = X9 "\/" Y9
proof
let L be with_infima Poset; ::_thesis: for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "/\" Y = X9 "\/" Y9
let X, Y be Subset of L; ::_thesis: for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "/\" Y = X9 "\/" Y9
let X9, Y9 be Subset of (L opp); ::_thesis: ( X = X9 & Y = Y9 implies X "/\" Y = X9 "\/" Y9 )
assume A1: ( X = X9 & Y = Y9 ) ; ::_thesis: X "/\" Y = X9 "\/" Y9
thus  X "/\" Y c= X9 "\/" Y9 :: according to XBOOLE_0:def_10 ::_thesis: X9 "\/" Y9 c= X "/\" Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "/\" Y or a in X9 "\/" Y9 )
assume  a in X "/\" Y ; ::_thesis: a in X9 "\/" Y9
then  a in  {  (p "/\" q) where p, q is Element of L : ( p in X & q in Y )  }  by YELLOW_4:def_4;
then consider x, y being Element of L such that
A2: a = x "/\" y and
A3: ( x in X & y in Y ) ;
A4: a = (x ~) "\/" (y ~) by A2, YELLOW_7:21;
 ( x ~ in X9 & y ~ in Y9 ) by A1, A3, LATTICE3:def_6;
then  a in  {  (p "\/" q) where p, q is Element of (L opp) : ( p in X9 & q in Y9 )  }  by A4;
hence  a in X9 "\/" Y9 by YELLOW_4:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X9 "\/" Y9 or a in X "/\" Y )
assume  a in X9 "\/" Y9 ; ::_thesis: a in X "/\" Y
then  a in  {  (p "\/" q) where p, q is Element of (L opp) : ( p in X9 & q in Y9 )  }  by YELLOW_4:def_3;
then consider x, y being Element of (L opp) such that
A5: a = x "\/" y and
A6: ( x in X9 & y in Y9 ) ;
A7: a = (~ x) "/\" (~ y) by A5, YELLOW_7:22;
 ( ~ x in X & ~ y in Y ) by A1, A6, LATTICE3:def_7;
then  a in  {  (p "/\" q) where p, q is Element of L : ( p in X & q in Y )  }  by A7;
hence  a in X "/\" Y by YELLOW_4:def_4; ::_thesis: verum
end;

theorem Th7: :: WAYBEL16:7
for L being non empty reflexive transitive RelStr holds Filt L = Ids (L opp)
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: Filt L = Ids (L opp)
A1: Ids (L opp) c= Filt L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ids (L opp) or x in Filt L )
assume  x in Ids (L opp) ; ::_thesis: x in Filt L
then  x in  {  X where X is Ideal of (L opp) : verum  }  by WAYBEL_0:def_23;
then consider x1 being Ideal of (L opp) such that
A2: x1 = x ;
 ( x1 is upper Subset of L & x1 is filtered Subset of L ) by YELLOW_7:27, YELLOW_7:29;
then  x in  {  X where X is Filter of L : verum  }  by A2;
hence  x in Filt L by WAYBEL_0:def_24; ::_thesis: verum
end;
 Filt L c= Ids (L opp)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Filt L or x in Ids (L opp) )
assume  x in Filt L ; ::_thesis: x in Ids (L opp)
then  x in  {  X where X is Filter of L : verum  }  by WAYBEL_0:def_24;
then consider x1 being Filter of L such that
A3: x1 = x ;
 ( x1 is lower Subset of (L opp) & x1 is directed Subset of (L opp) ) by YELLOW_7:27, YELLOW_7:29;
then  x in  {  X where X is Ideal of (L opp) : verum  }  by A3;
hence  x in Ids (L opp) by WAYBEL_0:def_23; ::_thesis: verum
end;
hence  Filt L = Ids (L opp) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL16:8
for L being non empty reflexive transitive RelStr holds Ids L = Filt (L opp)
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: Ids L = Filt (L opp)
A1: Filt (L opp) c= Ids L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Filt (L opp) or x in Ids L )
assume  x in Filt (L opp) ; ::_thesis: x in Ids L
then  x in  {  X where X is Filter of (L opp) : verum  }  by WAYBEL_0:def_24;
then consider x1 being Filter of (L opp) such that
A2: x1 = x ;
 ( x1 is lower Subset of L & x1 is directed Subset of L ) by YELLOW_7:26, YELLOW_7:28;
then  x in  {  X where X is Ideal of L : verum  }  by A2;
hence  x in Ids L by WAYBEL_0:def_23; ::_thesis: verum
end;
 Ids L c= Filt (L opp)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ids L or x in Filt (L opp) )
assume  x in Ids L ; ::_thesis: x in Filt (L opp)
then  x in  {  X where X is Ideal of L : verum  }  by WAYBEL_0:def_23;
then consider x1 being Ideal of L such that
A3: x1 = x ;
 ( x1 is upper Subset of (L opp) & x1 is filtered Subset of (L opp) ) by YELLOW_7:26, YELLOW_7:28;
then  x in  {  X where X is Filter of (L opp) : verum  }  by A3;
hence  x in Filt (L opp) by WAYBEL_0:def_24; ::_thesis: verum
end;
hence  Ids L = Filt (L opp) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

begin

definition
let S, T be non empty complete Poset;
mode CLHomomorphism of S,T ->  Function of S,T means :: WAYBEL16:def 1
( it is directed-sups-preserving & it is infs-preserving );
existence
 ex b1 being Function of S,T st
( b1 is directed-sups-preserving & b1 is infs-preserving )
proof
reconsider f = the carrier of S --> (Top T) as Function of the carrier of S, the carrier of T ;
reconsider f = f as Function of S,T ;
take  f ; ::_thesis: ( f is directed-sups-preserving & f is infs-preserving )
now__::_thesis:_for_X_being_Subset_of_S_st_not_X_is_empty_&_X_is_directed_holds_
f_preserves_sup_of_X
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; ::_thesis: f preserves_sup_of X
now__::_thesis:_(_ex_sup_of_X,S_implies_(_ex_sup_of_f_.:_X,T_&_sup_(f_.:_X)_=_f_._(sup_X)_)_)
assume  ex_sup_of X,S ; ::_thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
 rng f = {(Top T)} by FUNCOP_1:8;
then A2: f .: X c= {(Top T)} by RELAT_1:111;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
f_._x_<=_f_._y
let x, y be Element of S; ::_thesis: ( x <= y implies f . x <= f . y )
assume  x <= y ; ::_thesis: f . x <= f . y
f . x = Top T by FUNCOP_1:7
.= f . y by FUNCOP_1:7 ;
hence  f . x <= f . y ; ::_thesis: verum
end;
then  f is monotone by WAYBEL_1:def_2;
then A3: f .: X is non empty finite directed Subset of T by A1, A2, YELLOW_2:15;
hence  ex_sup_of f .: X,T by WAYBEL_0:75; ::_thesis: sup (f .: X) = f . (sup X)
 sup (f .: X) in f .: X by A3, WAYBEL_3:16;
then  sup (f .: X) = Top T by A2, TARSKI:def_1;
hence  sup (f .: X) = f . (sup X) by FUNCOP_1:7; ::_thesis: verum
end;
hence  f preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
hence  f is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: f is infs-preserving
now__::_thesis:_for_X_being_Subset_of_S_holds_f_preserves_inf_of_X
let X be Subset of S; ::_thesis: f preserves_inf_of X
now__::_thesis:_(_ex_inf_of_X,S_implies_(_ex_inf_of_f_.:_X,T_&_inf_(f_.:_X)_=_f_._(inf_X)_)_)
assume  ex_inf_of X,S ; ::_thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) )
thus  ex_inf_of f .: X,T by YELLOW_0:17; ::_thesis: inf (f .: X) = f . (inf X)
 rng f = {(Top T)} by FUNCOP_1:8;
then A4: f .: X is Subset of {(Top T)} by RELAT_1:111;
now__::_thesis:_inf_(f_.:_X)_=_f_._(inf_X)
percases ( f .: X = {} or f .: X <> {} ) ;
suppose f .: X = {} ; ::_thesis: inf (f .: X) = f . (inf X)
hence  inf (f .: X) = Top T by YELLOW_0:def_12
.= f . (inf X) by FUNCOP_1:7 ;
::_thesis: verum
end;
suppose f .: X <> {} ; ::_thesis: inf (f .: X) = f . (inf X)
then  f .: X = {(Top T)} by A4, ZFMISC_1:33;
hence  inf (f .: X) = Top T by YELLOW_0:39
.= f . (inf X) by FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;
hence  inf (f .: X) = f . (inf X) ; ::_thesis: verum
end;
hence  f preserves_inf_of X by WAYBEL_0:def_30; ::_thesis: verum
end;
hence  f is infs-preserving by WAYBEL_0:def_32; ::_thesis: verum
end;
end;

:: deftheorem  defines CLHomomorphism WAYBEL16:def_1_:_
 for S, T being non empty complete Poset
for b3 being Function of S,T holds
( b3 is CLHomomorphism of S,T iff ( b3 is directed-sups-preserving & b3 is infs-preserving ) );

definition
let S be non empty complete continuous Poset;
let A be Subset of S;
predA is_FG_set  means :: WAYBEL16:def 2
 for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) );
end;

:: deftheorem  defines is_FG_set WAYBEL16:def_2_:_
 for S being non empty complete continuous Poset
for A being Subset of S holds
( A is_FG_set iff for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );

registration
let L be non empty upper-bounded Poset;
cluster Filt L ->  non empty ;
coherence
 not Filt L is empty
proof
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_{(Top_L)}_&_x_<=_y_holds_
y_in_{(Top_L)}
let x, y be Element of L; ::_thesis: ( x in {(Top L)} & x <= y implies y in {(Top L)} )
assume that
A1: x in {(Top L)} and
A2: x <= y ; ::_thesis: y in {(Top L)}
 x = Top L by A1, TARSKI:def_1;
then  y = Top L by A2, WAYBEL15:3;
hence  y in {(Top L)} by TARSKI:def_1; ::_thesis: verum
end;
then  {(Top L)} is Filter of L by WAYBEL_0:5, WAYBEL_0:def_20;
then  {(Top L)} in  {  Y where Y is Filter of L : verum  }  ;
hence  not Filt L is empty by WAYBEL_0:def_24; ::_thesis: verum
end;
end;

theorem Th9: :: WAYBEL16:9
for X being set
for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)
proof
let X be set ; ::_thesis: for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)
set L = BoolePoset X;
let Y be non empty Subset of (InclPoset (Filt (BoolePoset X))); ::_thesis: meet Y is Filter of (BoolePoset X)
A1: now__::_thesis:_for_Z_being_set_st_Z_in_Y_holds_
Top_(BoolePoset_X)_in_Z
let Z be set ; ::_thesis: ( Z in Y implies Top (BoolePoset X) in Z )
assume  Z in Y ; ::_thesis: Top (BoolePoset X) in Z
then  Z in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then  Z in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then  Z in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then  ex Z1 being Filter of (BoolePoset X) st Z1 = Z ;
hence  Top (BoolePoset X) in Z by WAYBEL_4:22; ::_thesis: verum
end;
 Y c= the carrier of (InclPoset (Filt (BoolePoset X))) ;
then A2: Y c= the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
A3: for Z being Subset of (BoolePoset X) st Z in Y holds
Z is upper
proof
let Z be Subset of (BoolePoset X); ::_thesis: ( Z in Y implies Z is upper )
assume  Z in Y ; ::_thesis: Z is upper
then  Z in Filt (BoolePoset X) by A2;
then  Z in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then  ex Z1 being Filter of (BoolePoset X) st Z1 = Z ;
hence  Z is upper ; ::_thesis: verum
end;
A4: now__::_thesis:_for_V_being_Subset_of_(BoolePoset_X)_st_V_in_Y_holds_
(_V_is_upper_&_V_is_filtered_)
let V be Subset of (BoolePoset X); ::_thesis: ( V in Y implies ( V is upper & V is filtered ) )
assume  V in Y ; ::_thesis: ( V is upper & V is filtered )
then  V in Filt (BoolePoset X) by A2;
then  V in  {  Z where Z is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then A5: ex V1 being Filter of (BoolePoset X) st V1 = V ;
hence  V is upper ; ::_thesis: V is filtered
thus  V is filtered by A5; ::_thesis: verum
end;
 Y c= bool the carrier of (BoolePoset X)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Y or v in bool the carrier of (BoolePoset X) )
assume  v in Y ; ::_thesis: v in bool the carrier of (BoolePoset X)
then  v in Filt (BoolePoset X) by A2;
then  v in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then  ex v1 being Filter of (BoolePoset X) st v1 = v ;
hence  v in bool the carrier of (BoolePoset X) ; ::_thesis: verum
end;
hence  meet Y is Filter of (BoolePoset X) by A1, A3, A4, SETFAM_1:def_1, YELLOW_2:37, YELLOW_2:39; ::_thesis: verum
end;

theorem :: WAYBEL16:10
for X being set
for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds
( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
proof
let X be set ; ::_thesis: for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds
( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
set L = InclPoset (Filt (BoolePoset X));
let Y be non empty Subset of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
 meet Y is Filter of (BoolePoset X) by Th9;
then  meet Y in  {  Z where Z is Filter of (BoolePoset X) : verum  }  ;
then  meet Y in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def_24;
then reconsider a = meet Y as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_<=_than Y holds
b <= a
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b is_<=_than Y implies b <= a )
assume A2: b is_<=_than Y ; ::_thesis: b <= a
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
b_c=_x
let x be set ; ::_thesis: ( x in Y implies b c= x )
assume A3: x in Y ; ::_thesis: b c= x
then reconsider x9 = x as Element of (InclPoset (Filt (BoolePoset X))) ;
 b <= x9 by A2, A3, LATTICE3:def_8;
hence  b c= x by YELLOW_1:3; ::_thesis: verum
end;
then  b c= meet Y by SETFAM_1:5;
hence  b <= a by YELLOW_1:3; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_st_b_in_Y_holds_
a_<=_b
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b in Y implies a <= b )
assume  b in Y ; ::_thesis: a <= b
then  meet Y c= b by SETFAM_1:3;
hence  a <= b by YELLOW_1:3; ::_thesis: verum
end;
then  a is_<=_than Y by LATTICE3:def_8;
hence  ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y ) by A1, YELLOW_0:31; ::_thesis: verum
end;

theorem Th11: :: WAYBEL16:11
for X being set holds bool X is Filter of (BoolePoset X)
proof
let X be set ; ::_thesis: bool X is Filter of (BoolePoset X)
 bool X c= the carrier of (BoolePoset X) by WAYBEL_7:2;
then reconsider A = bool X as non empty Subset of (BoolePoset X) ;
A1: now__::_thesis:_for_x,_y_being_set_st_x_in_A_&_y_in_A_holds_
x_/\_y_in_A
let x, y be set ; ::_thesis: ( x in A & y in A implies x /\ y in A )
assume  ( x in A & y in A ) ; ::_thesis: x /\ y in A
then  x /\ y c= X /\ X by XBOOLE_1:27;
hence  x /\ y in A ; ::_thesis: verum
end;
 for x, y being set st x c= y & y c= X & x in A holds
y in A ;
then  A is upper by WAYBEL_7:7;
hence  bool X is Filter of (BoolePoset X) by A1, WAYBEL_7:9; ::_thesis: verum
end;

theorem Th12: :: WAYBEL16:12
for X being set holds {X} is Filter of (BoolePoset X)
proof
let X be set ; ::_thesis: {X} is Filter of (BoolePoset X)
now__::_thesis:_for_c_being_set_st_c_in_{X}_holds_
c_in_the_carrier_of_(BoolePoset_X)
let c be set ; ::_thesis: ( c in {X} implies c in the carrier of (BoolePoset X) )
assume  c in {X} ; ::_thesis: c in the carrier of (BoolePoset X)
then  c = X by TARSKI:def_1;
then  c is Element of (BoolePoset X) by WAYBEL_8:26;
hence  c in the carrier of (BoolePoset X) ; ::_thesis: verum
end;
then reconsider A = {X} as non empty Subset of (BoolePoset X) by TARSKI:def_3;
 for x, y being set st x c= y & y c= X & x in A holds
y in A
proof
let x, y be set ; ::_thesis: ( x c= y & y c= X & x in A implies y in A )
assume that
A1: ( x c= y & y c= X ) and
A2: x in A ; ::_thesis: y in A
 x = X by A2, TARSKI:def_1;
then  y = X by A1, XBOOLE_0:def_10;
hence  y in A by TARSKI:def_1; ::_thesis: verum
end;
then A3: A is upper by WAYBEL_7:7;
now__::_thesis:_for_x,_y_being_set_st_x_in_A_&_y_in_A_holds_
x_/\_y_in_A
let x, y be set ; ::_thesis: ( x in A & y in A implies x /\ y in A )
assume  ( x in A & y in A ) ; ::_thesis: x /\ y in A
then  ( x = X & y = X ) by TARSKI:def_1;
hence  x /\ y in A by TARSKI:def_1; ::_thesis: verum
end;
hence  {X} is Filter of (BoolePoset X) by A3, WAYBEL_7:9; ::_thesis: verum
end;

theorem :: WAYBEL16:13
for X being set holds InclPoset (Filt (BoolePoset X)) is upper-bounded
proof
let X be set ; ::_thesis: InclPoset (Filt (BoolePoset X)) is upper-bounded
set L = InclPoset (Filt (BoolePoset X));
 bool X is Filter of (BoolePoset X) by Th11;
then  bool X in  {  Z where Z is Filter of (BoolePoset X) : verum  }  ;
then  bool X in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def_24;
then reconsider x = bool X as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_st_b_in_the_carrier_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_
b_<=_x
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b in the carrier of (InclPoset (Filt (BoolePoset X))) implies b <= x )
assume  b in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: b <= x
then  b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then  b in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then  ex b1 being Filter of (BoolePoset X) st b1 = b ;
then  b c= the carrier of (BoolePoset X) ;
then  b c= bool X by WAYBEL_7:2;
hence  b <= x by YELLOW_1:3; ::_thesis: verum
end;
then  x is_>=_than the carrier of (InclPoset (Filt (BoolePoset X))) by LATTICE3:def_9;
hence  InclPoset (Filt (BoolePoset X)) is upper-bounded by YELLOW_0:def_5; ::_thesis: verum
end;

theorem :: WAYBEL16:14
for X being set holds InclPoset (Filt (BoolePoset X)) is lower-bounded
proof
let X be set ; ::_thesis: InclPoset (Filt (BoolePoset X)) is lower-bounded
set L = InclPoset (Filt (BoolePoset X));
 {X} is Filter of (BoolePoset X) by Th12;
then  {X} in  {  Z where Z is Filter of (BoolePoset X) : verum  }  ;
then  {X} in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def_24;
then reconsider x = {X} as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_st_b_in_the_carrier_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_
x_<=_b
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b in the carrier of (InclPoset (Filt (BoolePoset X))) implies x <= b )
assume  b in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: x <= b
then  b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then  b in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then consider b1 being Filter of (BoolePoset X) such that
A1: b1 = b ;
consider d being set  such that
A2: d in b1 by XBOOLE_0:def_1;
A3: d c= X by A2, WAYBEL_8:26;
now__::_thesis:_for_c_being_set_st_c_in_{X}_holds_
c_in_b
let c be set ; ::_thesis: ( c in {X} implies c in b )
assume  c in {X} ; ::_thesis: c in b
then  c = X by TARSKI:def_1;
hence  c in b by A1, A2, A3, WAYBEL_7:7; ::_thesis: verum
end;
then  {X} c= b by TARSKI:def_3;
hence  x <= b by YELLOW_1:3; ::_thesis: verum
end;
then  x is_<=_than the carrier of (InclPoset (Filt (BoolePoset X))) by LATTICE3:def_8;
hence  InclPoset (Filt (BoolePoset X)) is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;

theorem :: WAYBEL16:15
for X being set holds Top (InclPoset (Filt (BoolePoset X))) = bool X
proof
let X be set ; ::_thesis: Top (InclPoset (Filt (BoolePoset X))) = bool X
set L = InclPoset (Filt (BoolePoset X));
 bool X is Filter of (BoolePoset X) by Th11;
then  bool X in  {  Z where Z is Filter of (BoolePoset X) : verum  }  ;
then  bool X in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def_24;
then reconsider bX = bool X as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_<=_than {} holds
bX >= b
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b is_<=_than {} implies bX >= b )
assume  b is_<=_than {} ; ::_thesis: bX >= b
 b in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then  b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then  b in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then  ex b1 being Filter of (BoolePoset X) st b1 = b ;
then  b c= the carrier of (BoolePoset X) ;
then  b c= bool X by WAYBEL_7:2;
hence  bX >= b by YELLOW_1:3; ::_thesis: verum
end;
 bX is_<=_than {} by YELLOW_0:6;
then  "/\" ({},(InclPoset (Filt (BoolePoset X)))) = bool X by A1, YELLOW_0:31;
hence  Top (InclPoset (Filt (BoolePoset X))) = bool X by YELLOW_0:def_12; ::_thesis: verum
end;

theorem :: WAYBEL16:16
for X being set holds Bottom (InclPoset (Filt (BoolePoset X))) = {X}
proof
let X be set ; ::_thesis: Bottom (InclPoset (Filt (BoolePoset X))) = {X}
set L = InclPoset (Filt (BoolePoset X));
 {X} is Filter of (BoolePoset X) by Th12;
then  {X} in  {  Z where Z is Filter of (BoolePoset X) : verum  }  ;
then  {X} in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by WAYBEL_0:def_24;
then reconsider bX = {X} as Element of (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_>=_than {} holds
bX <= b
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b is_>=_than {} implies bX <= b )
assume  b is_>=_than {} ; ::_thesis: bX <= b
 b in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then  b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then  b in  {  V where V is Filter of (BoolePoset X) : verum  }  by WAYBEL_0:def_24;
then consider b1 being Filter of (BoolePoset X) such that
A2: b1 = b ;
consider d being set  such that
A3: d in b1 by XBOOLE_0:def_1;
A4: d c= X by A3, WAYBEL_8:26;
now__::_thesis:_for_c_being_set_st_c_in_{X}_holds_
c_in_b
let c be set ; ::_thesis: ( c in {X} implies c in b )
assume  c in {X} ; ::_thesis: c in b
then  c = X by TARSKI:def_1;
hence  c in b by A2, A3, A4, WAYBEL_7:7; ::_thesis: verum
end;
then  {X} c= b by TARSKI:def_3;
hence  bX <= b by YELLOW_1:3; ::_thesis: verum
end;
 bX is_>=_than {} by YELLOW_0:6;
then  "\/" ({},(InclPoset (Filt (BoolePoset X)))) = {X} by A1, YELLOW_0:30;
hence  Bottom (InclPoset (Filt (BoolePoset X))) = {X} by YELLOW_0:def_11; ::_thesis: verum
end;

theorem :: WAYBEL16:17
for X being non empty set
for Y being non empty 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 non empty Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
let Y be non empty 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 Th18: :: WAYBEL16:18
for L being upper-bounded Semilattice holds InclPoset (Filt L) is complete
proof
let L be upper-bounded Semilattice; ::_thesis: InclPoset (Filt L) is complete
 InclPoset (Ids (L opp)) is complete ;
hence  InclPoset (Filt L) is complete by Th7; ::_thesis: verum
end;

registration
let L be upper-bounded Semilattice;
cluster InclPoset (Filt L) ->  complete ;
coherence
 InclPoset (Filt L) is complete by Th18;
end;

begin

definition
let L be non empty RelStr ;
let p be Element of L;
attrp is completely-irreducible  means :Def3: :: WAYBEL16:def 3
 ex_min_of (uparrow p) \ {p},L;
end;

:: deftheorem Def3 defines completely-irreducible WAYBEL16:def_3_:_
 for L being non empty RelStr
for p being Element of L holds
( p is completely-irreducible iff ex_min_of (uparrow p) \ {p},L );

theorem Th19: :: WAYBEL16:19
for L being non empty RelStr
for p being Element of L st p is completely-irreducible holds
"/\" (((uparrow p) \ {p}),L) <> p
proof
let L be non empty RelStr ; ::_thesis: for p being Element of L st p is completely-irreducible holds
"/\" (((uparrow p) \ {p}),L) <> p
let p be Element of L; ::_thesis: ( p is completely-irreducible implies "/\" (((uparrow p) \ {p}),L) <> p )
assume  p is completely-irreducible ; ::_thesis: "/\" (((uparrow p) \ {p}),L) <> p
then  ex_min_of (uparrow p) \ {p},L by Def3;
then  "/\" (((uparrow p) \ {p}),L) in (uparrow p) \ {p} by WAYBEL_1:def_4;
then  not "/\" (((uparrow p) \ {p}),L) in {p} by XBOOLE_0:def_5;
hence  "/\" (((uparrow p) \ {p}),L) <> p by TARSKI:def_1; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
func Irr L ->  Subset of L means :Def4: :: WAYBEL16:def 4
 for x being Element of L holds
( x in it iff x is completely-irreducible );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is completely-irreducible )
proof
defpred S1[ Element of L] means $1 is completely-irreducible ;
consider X being Subset of L such that
A1: for x being Element of L holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
take  X ; ::_thesis: for x being Element of L holds
( x in X iff x is completely-irreducible )
thus  for x being Element of L holds
( x in X iff x is completely-irreducible ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is completely-irreducible ) ) & ( for x being Element of L holds
( x in b2 iff x is completely-irreducible ) ) holds
b1 = b2
proof
let S1, S2 be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in S1 iff x is completely-irreducible ) ) & ( for x being Element of L holds
( x in S2 iff x is completely-irreducible ) ) implies S1 = S2 )
assume that
A2: for x being Element of L holds
( x in S1 iff x is completely-irreducible ) and
A3: for x being Element of L holds
( x in S2 iff x is completely-irreducible ) ; ::_thesis: S1 = S2
now__::_thesis:_for_x1_being_set_holds_
(_(_x1_in_S1_implies_x1_in_S2_)_&_(_x1_in_S2_implies_x1_in_S1_)_)
let x1 be set ; ::_thesis: ( ( x1 in S1 implies x1 in S2 ) & ( x1 in S2 implies x1 in S1 ) )
thus  ( x1 in S1 implies x1 in S2 ) ::_thesis: ( x1 in S2 implies x1 in S1 )
proof
assume A4: x1 in S1 ; ::_thesis: x1 in S2
then reconsider x2 = x1 as Element of L ;
 x2 is completely-irreducible by A2, A4;
hence  x1 in S2 by A3; ::_thesis: verum
end;
thus  ( x1 in S2 implies x1 in S1 ) ::_thesis: verum
proof
assume A5: x1 in S2 ; ::_thesis: x1 in S1
then reconsider x2 = x1 as Element of L ;
 x2 is completely-irreducible by A3, A5;
hence  x1 in S1 by A2; ::_thesis: verum
end;
end;
hence  S1 = S2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Irr WAYBEL16:def_4_:_
 for L being non empty RelStr
for b2 being Subset of L holds
( b2 = Irr L iff for x being Element of L holds
( x in b2 iff x is completely-irreducible ) );

theorem Th20: :: WAYBEL16:20
for L being non empty Poset
for p being Element of L holds
( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )
proof
let L be non empty Poset; ::_thesis: for p being Element of L holds
( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )
let p be Element of L; ::_thesis: ( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )
thus  ( p is completely-irreducible implies ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) ) ::_thesis: ( ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) implies p is completely-irreducible )
proof
assume A1: p is completely-irreducible ; ::_thesis: ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) )
then  ex_min_of (uparrow p) \ {p},L by Def3;
then A2: ex_inf_of (uparrow p) \ {p},L by WAYBEL_1:def_4;
take q = "/\" (((uparrow p) \ {p}),L); ::_thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) )
now__::_thesis:_for_s_being_Element_of_L_st_s_in_(uparrow_p)_\_{p}_holds_
p_<=_s
let s be Element of L; ::_thesis: ( s in (uparrow p) \ {p} implies p <= s )
assume  s in (uparrow p) \ {p} ; ::_thesis: p <= s
then  s in uparrow p by XBOOLE_0:def_5;
hence  p <= s by WAYBEL_0:18; ::_thesis: verum
end;
then  p is_<=_than (uparrow p) \ {p} by LATTICE3:def_8;
then A3: p <= q by A2, YELLOW_0:def_10;
A4: {p} \/ (uparrow q) c= uparrow p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p} \/ (uparrow q) or x in uparrow p )
assume A5: x in {p} \/ (uparrow q) ; ::_thesis: x in uparrow p
now__::_thesis:_x_in_uparrow_p
percases ( x in {p} or x in uparrow q ) by A5, XBOOLE_0:def_3;
supposeA6: x in {p} ; ::_thesis: x in uparrow p
A7: p <= p ;
 x = p by A6, TARSKI:def_1;
hence  x in uparrow p by A7, WAYBEL_0:18; ::_thesis: verum
end;
supposeA8: x in uparrow q ; ::_thesis: x in uparrow p
then reconsider x1 = x as Element of L ;
 q <= x1 by A8, WAYBEL_0:18;
then  p <= x1 by A3, ORDERS_2:3;
hence  x in uparrow p by WAYBEL_0:18; ::_thesis: verum
end;
end;
end;
hence  x in uparrow p ; ::_thesis: verum
end;
 "/\" (((uparrow p) \ {p}),L) <> p by A1, Th19;
hence  p < q by A3, ORDERS_2:def_6; ::_thesis: ( ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) )
A9: q is_<=_than (uparrow p) \ {p} by A2, YELLOW_0:def_10;
thus  for s being Element of L st p < s holds
q <= s ::_thesis: uparrow p = {p} \/ (uparrow q)
proof
let s be Element of L; ::_thesis: ( p < s implies q <= s )
assume A10: p < s ; ::_thesis: q <= s
then  p <= s by ORDERS_2:def_6;
then A11: s in uparrow p by WAYBEL_0:18;
 not s in {p} by A10, TARSKI:def_1;
then  s in (uparrow p) \ {p} by A11, XBOOLE_0:def_5;
hence  q <= s by A9, LATTICE3:def_8; ::_thesis: verum
end;
 uparrow p c= {p} \/ (uparrow q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow p or x in {p} \/ (uparrow q) )
assume A12: x in uparrow p ; ::_thesis: x in {p} \/ (uparrow q)
then reconsider x1 = x as Element of L ;
 ( p = x1 or ( x1 in uparrow p & not x1 in {p} ) ) by A12, TARSKI:def_1;
then  ( p = x1 or x1 in (uparrow p) \ {p} ) by XBOOLE_0:def_5;
then  ( p = x1 or "/\" (((uparrow p) \ {p}),L) <= x1 ) by A9, LATTICE3:def_8;
then  ( x in {p} or x in uparrow q ) by TARSKI:def_1, WAYBEL_0:18;
hence  x in {p} \/ (uparrow q) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  uparrow p = {p} \/ (uparrow q) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) implies p is completely-irreducible ) ::_thesis: verum
proof
given q being Element of L such that A13: p < q and
A14: for s being Element of L st p < s holds
q <= s and
A15: uparrow p = {p} \/ (uparrow q) ; ::_thesis: p is completely-irreducible
A16: not q in {p} by A13, TARSKI:def_1;
 ex q being Element of L st
( (uparrow p) \ {p} is_>=_than q & ( for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b ) )
proof
take  q ; ::_thesis: ( (uparrow p) \ {p} is_>=_than q & ( for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b ) )
now__::_thesis:_for_a_being_Element_of_L_st_a_in_(uparrow_p)_\_{p}_holds_
q_<=_a
let a be Element of L; ::_thesis: ( a in (uparrow p) \ {p} implies q <= a )
assume A17: a in (uparrow p) \ {p} ; ::_thesis: q <= a
then  not a in {p} by XBOOLE_0:def_5;
then A18: a <> p by TARSKI:def_1;
 a in uparrow p by A17, XBOOLE_0:def_5;
then  p <= a by WAYBEL_0:18;
then  p < a by A18, ORDERS_2:def_6;
hence  q <= a by A14; ::_thesis: verum
end;
hence  (uparrow p) \ {p} is_>=_than q by LATTICE3:def_8; ::_thesis: for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b
let b be Element of L; ::_thesis: ( (uparrow p) \ {p} is_>=_than b implies q >= b )
assume A19: (uparrow p) \ {p} is_>=_than b ; ::_thesis: q >= b
 q <= q ;
then  q in uparrow q by WAYBEL_0:18;
then A20: q in {p} \/ (uparrow q) by XBOOLE_0:def_3;
 not q in {p} by A13, TARSKI:def_1;
then  q in (uparrow p) \ {p} by A15, A20, XBOOLE_0:def_5;
hence  q >= b by A19, LATTICE3:def_8; ::_thesis: verum
end;
then A21: ex_inf_of (uparrow p) \ {p},L by YELLOW_0:16;
A22: now__::_thesis:_for_b_being_Element_of_L_st_b_is_<=_than_(uparrow_p)_\_{p}_holds_
q_>=_b
let b be Element of L; ::_thesis: ( b is_<=_than (uparrow p) \ {p} implies q >= b )
assume A23: b is_<=_than (uparrow p) \ {p} ; ::_thesis: q >= b
 p <= q by A13, ORDERS_2:def_6;
then A24: q in uparrow p by WAYBEL_0:18;
 not q in {p} by A13, TARSKI:def_1;
then  q in (uparrow p) \ {p} by A24, XBOOLE_0:def_5;
hence  q >= b by A23, LATTICE3:def_8; ::_thesis: verum
end;
 p <= q by A13, ORDERS_2:def_6;
then A25: q in uparrow p by WAYBEL_0:18;
now__::_thesis:_for_c_being_Element_of_L_st_c_in_(uparrow_p)_\_{p}_holds_
q_<=_c
let c be Element of L; ::_thesis: ( c in (uparrow p) \ {p} implies q <= c )
assume  c in (uparrow p) \ {p} ; ::_thesis: q <= c
then  ( c in uparrow p & not c in {p} ) by XBOOLE_0:def_5;
then  c in uparrow q by A15, XBOOLE_0:def_3;
hence  q <= c by WAYBEL_0:18; ::_thesis: verum
end;
then  q is_<=_than (uparrow p) \ {p} by LATTICE3:def_8;
then  q = "/\" (((uparrow p) \ {p}),L) by A22, YELLOW_0:31;
then  "/\" (((uparrow p) \ {p}),L) in (uparrow p) \ {p} by A25, A16, XBOOLE_0:def_5;
then  ex_min_of (uparrow p) \ {p},L by A21, WAYBEL_1:def_4;
hence  p is completely-irreducible by Def3; ::_thesis: verum
end;
end;

theorem Th21: :: WAYBEL16:21
for L being non empty upper-bounded Poset holds not Top L in Irr L
proof
let L be non empty upper-bounded Poset; ::_thesis: not Top L in Irr L
assume  Top L in Irr L ; ::_thesis: contradiction
then  Top L is completely-irreducible by Def4;
then  "/\" (((uparrow (Top L)) \ {(Top L)}),L) <> Top L by Th19;
then  "/\" (({(Top L)} \ {(Top L)}),L) <> Top L by WAYBEL_4:24;
then  "/\" ({},L) <> Top L by XBOOLE_1:37;
hence  contradiction by YELLOW_0:def_12; ::_thesis: verum
end;

theorem Th22: :: WAYBEL16:22
for L being Semilattice holds Irr L c= IRR L
proof
let L be Semilattice; ::_thesis: Irr L c= IRR L
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Irr L or x in IRR L )
assume A1: x in Irr L ; ::_thesis: x in IRR L
then reconsider x1 = x as Element of L ;
 x1 is completely-irreducible by A1, Def4;
then consider q being Element of L such that
A2: x1 < q and
A3: for s being Element of L st x1 < s holds
q <= s and
 uparrow x1 = {x1} \/ (uparrow q) by Th20;
now__::_thesis:_for_a,_b_being_Element_of_L_st_x1_=_a_"/\"_b_&_a_<>_x1_holds_
not_b_<>_x1
let a, b be Element of L; ::_thesis: ( x1 = a "/\" b & a <> x1 implies not b <> x1 )
assume that
A4: x1 = a "/\" b and
A5: a <> x1 and
A6: b <> x1 ; ::_thesis: contradiction
 x1 <= b by A4, YELLOW_0:23;
then  x1 < b by A6, ORDERS_2:def_6;
then A7: q <= b by A3;
A8: x1 <= q by A2, ORDERS_2:def_6;
 x1 <= a by A4, YELLOW_0:23;
then  x1 < a by A5, ORDERS_2:def_6;
then  q <= a by A3;
then  q <= x1 by A4, A7, YELLOW_0:23;
hence  contradiction by A2, A8, ORDERS_2:2; ::_thesis: verum
end;
then  x1 is irreducible by WAYBEL_6:def_2;
hence  x in IRR L by WAYBEL_6:def_4; ::_thesis: verum
end;

theorem Th23: :: WAYBEL16:23
for L being Semilattice
for x being Element of L st x is completely-irreducible holds
x is irreducible
proof
let L be Semilattice; ::_thesis: for x being Element of L st x is completely-irreducible holds
x is irreducible
let x be Element of L; ::_thesis: ( x is completely-irreducible implies x is irreducible )
assume  x is completely-irreducible ; ::_thesis: x is irreducible
then A1: x in Irr L by Def4;
 Irr L c= IRR L by Th22;
hence  x is irreducible by A1, WAYBEL_6:def_4; ::_thesis: verum
end;

theorem Th24: :: WAYBEL16:24
for L being non empty Poset
for x being Element of L st x is completely-irreducible holds
for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
proof
let L be non empty Poset; ::_thesis: for x being Element of L st x is completely-irreducible holds
for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
let x be Element of L; ::_thesis: ( x is completely-irreducible implies for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X )
assume  x is completely-irreducible ; ::_thesis: for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
then consider q being Element of L such that
A1: x < q and
A2: for s being Element of L st x < s holds
q <= s and
 uparrow x = {x} \/ (uparrow q) by Th20;
let X be Subset of L; ::_thesis: ( ex_inf_of X,L & x = inf X implies x in X )
assume that
A3: ex_inf_of X,L and
A4: x = inf X and
A5: not x in X ; ::_thesis: contradiction
A6: X c= uparrow q
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in uparrow q )
assume A7: y in X ; ::_thesis: y in uparrow q
then reconsider y1 = y as Element of L ;
 inf X is_<=_than X by A3, YELLOW_0:31;
then  x <= y1 by A4, A7, LATTICE3:def_8;
then  x < y1 by A5, A7, ORDERS_2:def_6;
then  q <= y1 by A2;
hence  y in uparrow q by WAYBEL_0:18; ::_thesis: verum
end;
 ex_inf_of uparrow q,L by WAYBEL_0:39;
then  inf (uparrow q) <= inf X by A3, A6, YELLOW_0:35;
then  q <= x by A4, WAYBEL_0:39;
hence  contradiction by A1, ORDERS_2:6; ::_thesis: verum
end;

theorem Th25: :: WAYBEL16:25
for L being non empty Poset
for X being Subset of L st X is order-generating holds
Irr L c= X
proof
let L be non empty Poset; ::_thesis: for X being Subset of L st X is order-generating holds
Irr L c= X
let X be Subset of L; ::_thesis: ( X is order-generating implies Irr L c= X )
assume A1: X is order-generating ; ::_thesis: Irr L c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Irr L or x in X )
assume A2: x in Irr L ; ::_thesis: x in X
then reconsider x1 = x as Element of L ;
A3: ( x1 = "/\" (((uparrow x1) /\ X),L) & ex_inf_of (uparrow x1) /\ X,L ) by A1, WAYBEL_6:def_5;
 x1 is completely-irreducible by A2, Def4;
then  x1 in (uparrow x1) /\ X by A3, Th24;
hence  x in X by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th26: :: WAYBEL16:26
for L being complete LATTICE
for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds
p is completely-irreducible
proof
let L be complete LATTICE; ::_thesis: for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds
p is completely-irreducible
let p be Element of L; ::_thesis: ( ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) implies p is completely-irreducible )
given k being Element of L such that A1: p is_maximal_in the carrier of L \ (uparrow k) ; ::_thesis: p is completely-irreducible
 k <= p "\/" k by YELLOW_0:22;
then A2: p "\/" k in uparrow k by WAYBEL_0:18;
 p <= p "\/" k by YELLOW_0:22;
then  p "\/" k in uparrow p by WAYBEL_0:18;
then A3: ( ex_inf_of (uparrow p) \ {p},L & p "\/" k in (uparrow p) /\ (uparrow k) ) by A2, XBOOLE_0:def_4, YELLOW_0:17;
A4: (uparrow p) \ {p} = (uparrow p) /\ (uparrow k) by A1, Th3;
then  "/\" (((uparrow p) \ {p}),L) = p "\/" k by Th1;
then  ex_min_of (uparrow p) \ {p},L by A4, A3, WAYBEL_1:def_4;
hence  p is completely-irreducible by Def3; ::_thesis: verum
end;

theorem Th27: :: WAYBEL16:27
for L being transitive antisymmetric with_suprema RelStr
for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
p "\/" u = q "\/" u
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
p "\/" u = q "\/" u
let p, q, u be Element of L; ::_thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p implies p "\/" u = q "\/" u )
assume that
A1: p < q and
A2: for s being Element of L st p < s holds
q <= s and
A3: not u <= p ; ::_thesis: p "\/" u = q "\/" u
A4: q "\/" u >= q by YELLOW_0:22;
A5: now__::_thesis:_for_v_being_Element_of_L_st_v_>=_p_&_v_>=_u_holds_
q_"\/"_u_<=_v
let v be Element of L; ::_thesis: ( v >= p & v >= u implies q "\/" u <= v )
assume that
A6: v >= p and
A7: v >= u ; ::_thesis: q "\/" u <= v
 v > p by A3, A6, A7, ORDERS_2:def_6;
then  v >= q by A2;
hence  q "\/" u <= v by A7, YELLOW_0:22; ::_thesis: verum
end;
 p <= q by A1, ORDERS_2:def_6;
then A8: q "\/" u >= p by A4, ORDERS_2:3;
 q "\/" u >= u by YELLOW_0:22;
hence  p "\/" u = q "\/" u by A8, A5, YELLOW_0:22; ::_thesis: verum
end;

theorem Th28: :: WAYBEL16:28
for L being distributive LATTICE
for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
not u "/\" q <= p
proof
let L be distributive LATTICE; ::_thesis: for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
not u "/\" q <= p
let p, q, u be Element of L; ::_thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p implies not u "/\" q <= p )
assume that
A1: p < q and
A2: ( ( for s being Element of L st p < s holds
q <= s ) & not u <= p ) and
A3: u "/\" q <= p ; ::_thesis: contradiction
A4: p <= q by A1, ORDERS_2:def_6;
p = p "\/" (u "/\" q) by A3, YELLOW_0:24
.= (p "\/" u) "/\" (q "\/" p) by WAYBEL_1:5
.= (p "\/" u) "/\" q by A4, YELLOW_0:24
.= q "/\" (q "\/" u) by A1, A2, Th27
.= q by LATTICE3:18 ;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th29: :: WAYBEL16:29
for L being distributive complete LATTICE st L opp is meet-continuous holds
for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L
proof
let L be distributive complete LATTICE; ::_thesis: ( L opp is meet-continuous implies for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L )
assume A1: L opp is meet-continuous ; ::_thesis: for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L
let p be Element of L; ::_thesis: ( p is completely-irreducible implies the carrier of L \ (downarrow p) is Open Filter of L )
assume A2: p is completely-irreducible ; ::_thesis: the carrier of L \ (downarrow p) is Open Filter of L
then consider q being Element of L such that
A3: p < q and
A4: for s being Element of L st p < s holds
q <= s and
 uparrow p = {p} \/ (uparrow q) by Th20;
defpred S1[ Element of L] means ( $1 <= q & not $1 <= p );
reconsider F =  {  t where t is Element of L : S1[t]  }  as Subset of L from DOMAIN_1:sch_7();
 not q <= p by A3, ORDERS_2:6;
then A5: q in F ;
A6: now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_F_&_y_in_F_holds_
ex_z_being_Element_of_the_carrier_of_L_st_
(_z_in_F_&_z_<=_x_&_z_<=_y_)
let x, y be Element of L; ::_thesis: ( x in F & y in F implies ex z being Element of the carrier of L st
( z in F & z <= x & z <= y ) )
assume that
A7: x in F and
A8: y in F ; ::_thesis: ex z being Element of the carrier of L st
( z in F & z <= x & z <= y )
A9: ex x1 being Element of L st
( x1 = x & x1 <= q & not x1 <= p ) by A7;
take z = x "/\" y; ::_thesis: ( z in F & z <= x & z <= y )
A10: z <= x by YELLOW_0:23;
A11: ex y1 being Element of L st
( y1 = y & y1 <= q & not y1 <= p ) by A8;
A12: not z <= p
proof
A13: now__::_thesis:_for_d_being_Element_of_L_st_d_>=_y_&_d_>=_p_holds_
q_<=_d
let d be Element of L; ::_thesis: ( d >= y & d >= p implies q <= d )
assume  ( d >= y & d >= p ) ; ::_thesis: q <= d
then  d > p by A11, ORDERS_2:def_6;
hence  q <= d by A4; ::_thesis: verum
end;
assume A14: z <= p ; ::_thesis: contradiction
A15: q >= p by A3, ORDERS_2:def_6;
x = x "/\" q by A9, YELLOW_0:25
.= x "/\" (y "\/" p) by A11, A15, A13, YELLOW_0:22
.= z "\/" (x "/\" p) by WAYBEL_1:def_3
.= (x "\/" z) "/\" (z "\/" p) by WAYBEL_1:5
.= x "/\" (p "\/" z) by A10, YELLOW_0:24
.= x "/\" p by A14, YELLOW_0:24 ;
hence  contradiction by A9, YELLOW_0:25; ::_thesis: verum
end;
 z <= q by A9, A10, ORDERS_2:3;
hence  z in F by A12; ::_thesis: ( z <= x & z <= y )
thus  z <= x by YELLOW_0:23; ::_thesis: z <= y
thus  z <= y by YELLOW_0:23; ::_thesis: verum
end;
 p is irreducible by A2, Th23;
then A16: p is prime by WAYBEL_6:27;
 not Top L in Irr L by Th21;
then  p <> Top L by A2, Def4;
then  (downarrow p) ` is Filter of L by A16, WAYBEL_6:26;
then reconsider V = the carrier of L \ (downarrow p) as Filter of L by SUBSET_1:def_4;
reconsider F = F as non empty filtered Subset of L by A5, A6, WAYBEL_0:def_2;
reconsider F1 = F as non empty directed Subset of (L opp) by YELLOW_7:27;
now__::_thesis:_for_x_being_Element_of_L_st_x_in_V_holds_
ex_y_being_Element_of_the_carrier_of_L_st_
(_y_in_V_&_y_<<_x_)
let x be Element of L; ::_thesis: ( x in V implies ex y being Element of the carrier of L st
( y in V & y << x ) )
assume A17: x in V ; ::_thesis: ex y being Element of the carrier of L st
( y in V & y << x )
take y = inf F; ::_thesis: ( y in V & y << x )
thus  y in V ::_thesis: y << x
proof
now__::_thesis:_for_r_being_Element_of_L_st_r_in_{p}_"\/"_F_holds_
q_<=_r
let r be Element of L; ::_thesis: ( r in {p} "\/" F implies q <= r )
assume  r in {p} "\/" F ; ::_thesis: q <= r
then  r in  {  (p "\/" v) where v is Element of L : v in F  }  by YELLOW_4:15;
then consider v being Element of L such that
A18: r = p "\/" v and
A19: v in F ;
 ex v1 being Element of L st
( v = v1 & v1 <= q & not v1 <= p ) by A19;
then A20: p <> r by A18, YELLOW_0:24;
 p <= r by A18, YELLOW_0:22;
then  p < r by A20, ORDERS_2:def_6;
hence  q <= r by A4; ::_thesis: verum
end;
then A21: q is_<=_than {p} "\/" F by LATTICE3:def_8;
A22: ex_inf_of {(p ~)} "/\" F1,L by YELLOW_0:17;
 ex_inf_of F,L by YELLOW_0:17;
then A23: inf F = sup F1 by YELLOW_7:13;
A24: {(p ~)} = {p} by LATTICE3:def_6;
assume  not y in V ; ::_thesis: contradiction
then  y in downarrow p by XBOOLE_0:def_5;
then  y <= p by WAYBEL_0:17;
then p = p "\/" y by YELLOW_0:24
.= (p ~) "/\" ((inf F) ~) by YELLOW_7:23
.= (p ~) "/\" (sup F1) by A23, LATTICE3:def_6
.= sup ({(p ~)} "/\" F1) by A1, WAYBEL_2:def_6
.= "/\" (({(p ~)} "/\" F1),L) by A22, YELLOW_7:13
.= "/\" (({p} "\/" F),L) by A24, Th5 ;
then  q <= p by A21, YELLOW_0:33;
hence  contradiction by A3, ORDERS_2:6; ::_thesis: verum
end;
then  not y in downarrow p by XBOOLE_0:def_5;
then A25: not y <= p by WAYBEL_0:17;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_L_st_y_<=_sup_D_holds_
ex_d_being_Element_of_L_st_
(_d_in_D_&_y_<=_d_)
let D be non empty directed Subset of L; ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & y <= d ) )
assume A26: y <= sup D ; ::_thesis: ex d being Element of L st
( d in D & y <= d )
 not D \ (downarrow p) is empty
proof
assume  D \ (downarrow p) is empty ; ::_thesis: contradiction
then  D c= downarrow p by XBOOLE_1:37;
then  sup D <= sup (downarrow p) by WAYBEL_7:1;
then  y <= sup (downarrow p) by A26, ORDERS_2:3;
hence  contradiction by A25, WAYBEL_0:34; ::_thesis: verum
end;
then consider d being set  such that
A27: d in D \ (downarrow p) by XBOOLE_0:def_1;
reconsider d = d as Element of L by A27;
take d = d; ::_thesis: ( d in D & y <= d )
thus  d in D by A27, XBOOLE_0:def_5; ::_thesis: y <= d
 not d in downarrow p by A27, XBOOLE_0:def_5;
then  not d <= p by WAYBEL_0:17;
then  ( d "/\" q <= q & not d "/\" q <= p ) by A3, A4, Th28, YELLOW_0:23;
then  ( y is_<=_than F & d "/\" q in F ) by YELLOW_0:33;
then  ( d "/\" q <= d & y <= d "/\" q ) by LATTICE3:def_8, YELLOW_0:23;
hence  y <= d by ORDERS_2:3; ::_thesis: verum
end;
then A28: y << y by WAYBEL_3:def_1;
 not x in downarrow p by A17, XBOOLE_0:def_5;
then  not x <= p by WAYBEL_0:17;
then  ( x "/\" q <= q & not x "/\" q <= p ) by A3, A4, Th28, YELLOW_0:23;
then  ( y is_<=_than F & x "/\" q in F ) by YELLOW_0:33;
then  ( x "/\" q <= x & y <= x "/\" q ) by LATTICE3:def_8, YELLOW_0:23;
then  y <= x by ORDERS_2:3;
hence  y << x by A28, WAYBEL_3:2; ::_thesis: verum
end;
hence  the carrier of L \ (downarrow p) is Open Filter of L by WAYBEL_6:def_1; ::_thesis: verum
end;

theorem :: WAYBEL16:30
for L being distributive complete LATTICE st L opp is meet-continuous holds
for p being Element of L st p is completely-irreducible holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
proof
let L be distributive complete LATTICE; ::_thesis: ( L opp is meet-continuous implies for p being Element of L st p is completely-irreducible holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
assume A1: L opp is meet-continuous ; ::_thesis: for p being Element of L st p is completely-irreducible holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
let p be Element of L; ::_thesis: ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
assume A2: p is completely-irreducible ; ::_thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
then reconsider V = the carrier of L \ (downarrow p) as Open Filter of L by A1, Th29;
now__::_thesis:_for_b_being_Element_of_L_st_b_in_(uparrow_p)_\_{p}_holds_
p_<=_b
let b be Element of L; ::_thesis: ( b in (uparrow p) \ {p} implies p <= b )
assume  b in (uparrow p) \ {p} ; ::_thesis: p <= b
then  b in uparrow p by XBOOLE_0:def_5;
hence  p <= b by WAYBEL_0:18; ::_thesis: verum
end;
then  p is_<=_than (uparrow p) \ {p} by LATTICE3:def_8;
then A3: p <= "/\" (((uparrow p) \ {p}),L) by YELLOW_0:33;
 "/\" (((uparrow p) \ {p}),L) <> p by A2, Th19;
then A4: p < "/\" (((uparrow p) \ {p}),L) by A3, ORDERS_2:def_6;
A5: ( ex_inf_of V,L & (inf V) ~ = inf V ) by LATTICE3:def_6, YELLOW_0:17;
take k = inf V; ::_thesis: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
reconsider V9 = V as non empty directed Subset of (L opp) by YELLOW_7:27;
A6: ex_inf_of {(p ~)} "/\" V9,L by YELLOW_0:17;
A7: ( ex_inf_of {p} "\/" V,L & ex_inf_of (uparrow p) \ {p},L ) by YELLOW_0:17;
A8: {p} "\/" V c= (uparrow p) \ {p}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p} "\/" V or x in (uparrow p) \ {p} )
assume  x in {p} "\/" V ; ::_thesis: x in (uparrow p) \ {p}
then  x in  {  (p "\/" v) where v is Element of L : v in V  }  by YELLOW_4:15;
then consider v being Element of L such that
A9: x = p "\/" v and
A10: v in V ;
 not v in downarrow p by A10, XBOOLE_0:def_5;
then  not v <= p by WAYBEL_0:17;
then  p "\/" v <> p by YELLOW_0:22;
then A11: not p "\/" v in {p} by TARSKI:def_1;
 p <= p "\/" v by YELLOW_0:22;
then  p "\/" v in uparrow p by WAYBEL_0:18;
hence  x in (uparrow p) \ {p} by A9, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
A12: p = p ~ by LATTICE3:def_6;
p "\/" k = (p ~) "/\" ((inf V) ~) by YELLOW_7:23
.= (p ~) "/\" ("\/" (V,(L opp))) by A5, YELLOW_7:13
.= "\/" (({(p ~)} "/\" V9),(L opp)) by A1, WAYBEL_2:def_6
.= "/\" (({(p ~)} "/\" V9),L) by A6, YELLOW_7:13
.= inf ({p} "\/" V) by A12, Th5 ;
then A13: "/\" (((uparrow p) \ {p}),L) <= p "\/" k by A7, A8, YELLOW_0:35;
A14: not k <= p
proof
assume  k <= p ; ::_thesis: contradiction
then  p "\/" k = p by YELLOW_0:24;
hence  contradiction by A13, A4, ORDERS_2:7; ::_thesis: verum
end;
 uparrow k = V
proof
thus  uparrow k c= V :: according to XBOOLE_0:def_10 ::_thesis: V c= uparrow k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow k or x in V )
assume A15: x in uparrow k ; ::_thesis: x in V
then reconsider x1 = x as Element of L ;
 k <= x1 by A15, WAYBEL_0:18;
then  not x1 <= p by A14, ORDERS_2:3;
then  not x1 in downarrow p by WAYBEL_0:17;
hence  x in V by XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in uparrow k )
assume A16: x in V ; ::_thesis: x in uparrow k
then reconsider x1 = x as Element of L ;
 k is_<=_than V by YELLOW_0:33;
then  k <= x1 by A16, LATTICE3:def_8;
hence  x in uparrow k by WAYBEL_0:18; ::_thesis: verum
end;
then  k is compact by WAYBEL_8:2;
hence  k in the carrier of (CompactSublatt L) by WAYBEL_8:def_1; ::_thesis: p is_maximal_in the carrier of L \ (uparrow k)
A17: for y being Element of L holds
( not y in the carrier of L \ (uparrow k) or not p < y )
proof
given y being Element of L such that A18: y in the carrier of L \ (uparrow k) and
A19: p < y ; ::_thesis: contradiction
 not y in uparrow k by A18, XBOOLE_0:def_5;
then  ( k is_<=_than V & not k <= y ) by WAYBEL_0:18, YELLOW_0:33;
then  not y in V by LATTICE3:def_8;
then  y in downarrow p by XBOOLE_0:def_5;
then  y <= p by WAYBEL_0:17;
hence  contradiction by A19, ORDERS_2:6; ::_thesis: verum
end;
 not p in uparrow k by A14, WAYBEL_0:18;
then  p in the carrier of L \ (uparrow k) by XBOOLE_0:def_5;
hence  p is_maximal_in the carrier of L \ (uparrow k) by A17, WAYBEL_4:55; ::_thesis: verum
end;

theorem Th31: :: WAYBEL16:31
for L being lower-bounded algebraic LATTICE
for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p ) )
assume A1: not y <= x ; ::_thesis: ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
 for z being Element of L holds
( not waybelow z is empty & waybelow z is directed ) ;
then consider k1 being Element of L such that
A2: k1 << y and
A3: not k1 <= x by A1, WAYBEL_3:24;
consider k being Element of L such that
A4: k in the carrier of (CompactSublatt L) and
A5: k1 <= k and
A6: k <= y by A2, WAYBEL_8:7;
 not k <= x by A3, A5, ORDERS_2:3;
then  not x in uparrow k by WAYBEL_0:18;
then  x in the carrier of L \ (uparrow k) by XBOOLE_0:def_5;
then A7: x in (uparrow k) ` by SUBSET_1:def_4;
 k is compact by A4, WAYBEL_8:def_1;
then  uparrow k is Open Filter of L by WAYBEL_8:2;
then consider p being Element of L such that
A8: x <= p and
A9: p is_maximal_in (uparrow k) ` by A7, WAYBEL_6:9;
take  p ; ::_thesis: ( p is completely-irreducible & x <= p & not y <= p )
 the carrier of L \ (uparrow k) = (uparrow k) ` by SUBSET_1:def_4;
hence  p is completely-irreducible by A9, Th26; ::_thesis: ( x <= p & not y <= p )
thus  x <= p by A8; ::_thesis: not y <= p
thus  not y <= p ::_thesis: verum
proof
 p in (uparrow k) ` by A9, WAYBEL_4:55;
then  p in the carrier of L \ (uparrow k) by SUBSET_1:def_4;
then A10: not p in uparrow k by XBOOLE_0:def_5;
assume  y <= p ; ::_thesis: contradiction
then  k <= p by A6, ORDERS_2:3;
hence  contradiction by A10, WAYBEL_0:18; ::_thesis: verum
end;
end;

theorem Th32: :: WAYBEL16:32
for L being lower-bounded algebraic LATTICE holds
( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds
Irr L c= X ) )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: ( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds
Irr L c= X ) )
now__::_thesis:_for_x,_y_being_Element_of_L_st_not_y_<=_x_holds_
ex_p_being_Element_of_L_st_
(_p_in_Irr_L_&_x_<=_p_&_not_y_<=_p_)
let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st
( p in Irr L & x <= p & not y <= p ) )
assume  not y <= x ; ::_thesis: ex p being Element of L st
( p in Irr L & x <= p & not y <= p )
then consider p being Element of L such that
A1: p is completely-irreducible and
A2: x <= p and
A3: not y <= p by Th31;
take p = p; ::_thesis: ( p in Irr L & x <= p & not y <= p )
thus  p in Irr L by A1, Def4; ::_thesis: ( x <= p & not y <= p )
thus  x <= p by A2; ::_thesis: not y <= p
thus  not y <= p by A3; ::_thesis: verum
end;
hence  Irr L is order-generating by WAYBEL_6:17; ::_thesis: for X being Subset of L st X is order-generating holds
Irr L c= X
let X be Subset of L; ::_thesis: ( X is order-generating implies Irr L c= X )
assume  X is order-generating ; ::_thesis: Irr L c= X
hence  Irr L c= X by Th25; ::_thesis: verum
end;

theorem :: WAYBEL16:33
for L being lower-bounded algebraic LATTICE
for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)
let s be Element of L; ::_thesis: s = "/\" (((uparrow s) /\ (Irr L)),L)
 Irr L is order-generating by Th32;
hence  s = "/\" (((uparrow s) /\ (Irr L)),L) by WAYBEL_6:def_5; ::_thesis: verum
end;

theorem Th34: :: WAYBEL16:34
for L being non empty complete Poset
for X being Subset of L
for p being Element of L st p is completely-irreducible & p = inf X holds
p in X
proof
let L be non empty complete Poset; ::_thesis: for X being Subset of L
for p being Element of L st p is completely-irreducible & p = inf X holds
p in X
let X be Subset of L; ::_thesis: for p being Element of L st p is completely-irreducible & p = inf X holds
p in X
let p be Element of L; ::_thesis: ( p is completely-irreducible & p = inf X implies p in X )
assume that
A1: p is completely-irreducible and
A2: p = inf X ; ::_thesis: p in X
assume A3: not p in X ; ::_thesis: contradiction
consider q being Element of L such that
A4: p < q and
A5: for s being Element of L st p < s holds
q <= s and
 uparrow p = {p} \/ (uparrow q) by A1, Th20;
A6: p is_<=_than X by A2, YELLOW_0:33;
now__::_thesis:_for_b_being_Element_of_L_st_b_in_X_holds_
q_<=_b
let b be Element of L; ::_thesis: ( b in X implies q <= b )
assume A7: b in X ; ::_thesis: q <= b
then  p <= b by A6, LATTICE3:def_8;
then  p < b by A3, A7, ORDERS_2:def_6;
hence  q <= b by A5; ::_thesis: verum
end;
then A8: q is_<=_than X by LATTICE3:def_8;
A9: p <= q by A4, ORDERS_2:def_6;
now__::_thesis:_for_b_being_Element_of_L_st_b_is_<=_than_X_holds_
q_>=_b
let b be Element of L; ::_thesis: ( b is_<=_than X implies q >= b )
assume  b is_<=_than X ; ::_thesis: q >= b
then  p >= b by A2, YELLOW_0:33;
hence  q >= b by A9, ORDERS_2:3; ::_thesis: verum
end;
hence  contradiction by A2, A4, A8, YELLOW_0:33; ::_thesis: verum
end;

theorem Th35: :: WAYBEL16:35
for L being complete algebraic LATTICE
for p being Element of L st p is completely-irreducible holds
p = "/\" ( {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ,L)
proof
let L be complete algebraic LATTICE; ::_thesis: for p being Element of L st p is completely-irreducible holds
p = "/\" ( {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ,L)
let p be Element of L; ::_thesis: ( p is completely-irreducible implies p = "/\" ( {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ,L) )
set A =  {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ;
 p <= p ;
then A1: p in uparrow p by WAYBEL_0:18;
now__::_thesis:_for_a_being_Element_of_L_st_a_in__{__x_where_x_is_Element_of_L_:_(_x_in_uparrow_p_&_ex_k_being_Element_of_L_st_
(_k_in_the_carrier_of_(CompactSublatt_L)_&_x_is_maximal_in_the_carrier_of_L_\_(uparrow_k)_)_)__}__holds_
p_<=_a
let a be Element of L; ::_thesis: ( a in  {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  implies p <= a )
assume  a in  {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ; ::_thesis: p <= a
then  ex a1 being Element of L st
( a1 = a & a1 in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & a1 is_maximal_in the carrier of L \ (uparrow k) ) ) ;
hence  p <= a by WAYBEL_0:18; ::_thesis: verum
end;
then A2: p is_<=_than  {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  by LATTICE3:def_8;
assume  p is completely-irreducible ; ::_thesis: p = "/\" ( {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ,L)
then consider q being Element of L such that
A3: p < q and
A4: for s being Element of L st p < s holds
q <= s and
 uparrow p = {p} \/ (uparrow q) by Th20;
A5: compactbelow p <> compactbelow q
proof
assume  compactbelow p = compactbelow q ; ::_thesis: contradiction
then p = sup (compactbelow q) by WAYBEL_8:def_3
.= q by WAYBEL_8:def_3 ;
hence  contradiction by A3; ::_thesis: verum
end;
 p <= q by A3, ORDERS_2:def_6;
then  compactbelow p c= compactbelow q by WAYBEL13:1;
then  not compactbelow q c= compactbelow p by A5, XBOOLE_0:def_10;
then consider k1 being set  such that
A6: k1 in compactbelow q and
A7: not k1 in compactbelow p by TARSKI:def_3;
 k1 in  {  y where y is Element of L : ( q >= y & y is compact )  }  by A6, WAYBEL_8:def_2;
then consider k being Element of L such that
A8: k = k1 and
A9: q >= k and
A10: k is compact ;
A11: for y being Element of L holds
( not y in the carrier of L \ (uparrow k) or not p < y )
proof
given y being Element of L such that A12: y in the carrier of L \ (uparrow k) and
A13: p < y ; ::_thesis: contradiction
 q <= y by A4, A13;
then  k <= y by A9, ORDERS_2:3;
then  y in uparrow k by WAYBEL_0:18;
hence  contradiction by A12, XBOOLE_0:def_5; ::_thesis: verum
end;
 not k <= p by A7, A8, A10, WAYBEL_8:4;
then  not p in uparrow k by WAYBEL_0:18;
then  p in the carrier of L \ (uparrow k) by XBOOLE_0:def_5;
then A14: p is_maximal_in the carrier of L \ (uparrow k) by A11, WAYBEL_4:55;
 k in the carrier of (CompactSublatt L) by A10, WAYBEL_8:def_1;
then  p in  {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  by A1, A14;
then  for u being Element of L st u is_<=_than  {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  holds
p >= u by LATTICE3:def_8;
hence  p = "/\" ( {  x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) )  }  ,L) by A2, YELLOW_0:33; ::_thesis: verum
end;

theorem :: WAYBEL16:36
for L being complete algebraic LATTICE
for p being Element of L holds
( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )
proof
let L be complete algebraic LATTICE; ::_thesis: for p being Element of L holds
( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )
let p be Element of L; ::_thesis: ( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )
thus  ( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) implies p is completely-irreducible ) by Th26; ::_thesis: ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
thus  ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) ) ::_thesis: verum
proof
defpred S1[ Element of L] means ( $1 in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & $1 is_maximal_in the carrier of L \ (uparrow k) ) );
reconsider A =  {  x where x is Element of L : S1[x]  }  as Subset of L from DOMAIN_1:sch_7();
assume A1: p is completely-irreducible ; ::_thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
then  p = inf A by Th35;
then  p in A by A1, Th34;
then consider x being Element of L such that
A2: x = p and
 x in uparrow p and
A3: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ;
consider k being Element of L such that
A4: k in the carrier of (CompactSublatt L) and
A5: x is_maximal_in the carrier of L \ (uparrow k) by A3;
take  k ; ::_thesis: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
thus  k in the carrier of (CompactSublatt L) by A4; ::_thesis: p is_maximal_in the carrier of L \ (uparrow k)
thus  p is_maximal_in the carrier of L \ (uparrow k) by A2, A5; ::_thesis: verum
end;
end;