:: LATTICE6 semantic presentation

begin

registration
cluster non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for LattStr ;
existence
 ex b1 being Lattice st b1 is finite
proof
set L = BooleLatt {};
 the carrier of (BooleLatt {}) = bool {} by LATTICE3:def_1;
then  BooleLatt {} is finite ;
hence  ex b1 being Lattice st b1 is finite ; ::_thesis: verum
end;
end;

Lm1:  for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
proof
defpred S1[ Element of NAT ] means  for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = $1 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) );
let L be finite Lattice; ::_thesis: for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
let X be Subset of L; ::_thesis: ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
percases ( k = 0 or k <> 0 ) ;
supposeA3: k = 0 ; ::_thesis: S1[k + 1]
 for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = 1 implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
assume that
A4: rng p = X and
A5: len p = 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
consider a being set  such that
A6: p . 1 = a ;
A7: Seg 1 = dom p by A5, FINSEQ_1:def_3;
then  1 in dom p by FINSEQ_1:2, TARSKI:def_1;
then A8: a in rng p by A6, FUNCT_1:def_3;
then reconsider a = a as Element of (LattPOSet L) by A4;
 rng p = {a} by A7, A6, FINSEQ_1:2, FUNCT_1:4;
then  for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a by A4, TARSKI:def_1;
hence  ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) by A4, A8; ::_thesis: verum
end;
hence  S1[k + 1] by A3; ::_thesis: verum
end;
supposeA9: k <> 0 ; ::_thesis: S1[k + 1]
 for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
assume that
A10: rng p = X and
A11: len p = k + 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
set q = p | (Seg k);
set X9 = rng (p | (Seg k));
A12: rng (p | (Seg k)) c= rng p by RELAT_1:70;
 for x being set st x in rng (p | (Seg k)) holds
x in the carrier of (LattPOSet L)
proof
let x be set ; ::_thesis: ( x in rng (p | (Seg k)) implies x in the carrier of (LattPOSet L) )
assume  x in rng (p | (Seg k)) ; ::_thesis: x in the carrier of (LattPOSet L)
then  x in rng p by A12;
hence  x in the carrier of (LattPOSet L) by A10; ::_thesis: verum
end;
then A13: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def_3;
A14: k <= len p by A11, NAT_1:11;
then  ( len (p | (Seg k)) = k & p | (Seg k) <> {} ) by A9, CARD_1:27, FINSEQ_1:17;
then consider a being Element of (LattPOSet L) such that
A15: a in rng (p | (Seg k)) and
A16: for b being Element of (LattPOSet L) st b in rng (p | (Seg k)) & b <> a holds
not b <= a by A2, A13;
consider b being set  such that
A17: p . (k + 1) = b ;
 Seg (k + 1) = dom p by A11, FINSEQ_1:def_3;
then  k + 1 in dom p by FINSEQ_1:4;
then A18: b in rng p by A17, FUNCT_1:def_3;
then reconsider b = b as Element of (LattPOSet L) by A10;
percases ( ex c being Element of (LattPOSet L) st
( c in X & c <= b & c <> b ) or for c being Element of (LattPOSet L) holds
( not c in X or not c <= b or not c <> b ) ) ;
suppose ex c being Element of (LattPOSet L) st
( c in X & c <= b & c <> b ) ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
then consider c being Element of (LattPOSet L) such that
A19: c in X and
A20: c <= b and
A21: c <> b ;
 for u being Element of (LattPOSet L) st u in X & u <> a holds
not u <= a
proof
let u be Element of (LattPOSet L); ::_thesis: ( u in X & u <> a implies not u <= a )
assume that
A22: u in X and
A23: u <> a ; ::_thesis: not u <= a
percases ( u in rng (p | (Seg k)) or not u in rng (p | (Seg k)) ) ;
suppose u in rng (p | (Seg k)) ; ::_thesis: not u <= a
hence  not u <= a by A16, A23; ::_thesis: verum
end;
supposeA24: not u in rng (p | (Seg k)) ; ::_thesis: not u <= a
consider n being set  such that
A25: n in dom p and
A26: p . n = u by A10, A22, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A25;
A27: Seg (k + 1) = dom p by A11, FINSEQ_1:def_3;
then A28: n <= k + 1 by A25, FINSEQ_1:1;
A29: 1 <= n by A25, A27, FINSEQ_1:1;
A30: n = k + 1
proof
assume  n <> k + 1 ; ::_thesis: contradiction
then  n < k + 1 by A28, XXREAL_0:1;
then  n <= k by NAT_1:13;
then  n in Seg k by A29, FINSEQ_1:1;
then A31: n in dom (p | (Seg k)) by A14, FINSEQ_1:17;
then  (p | (Seg k)) . n = u by A26, FUNCT_1:47;
hence  contradiction by A24, A31, FUNCT_1:def_3; ::_thesis: verum
end;
A32: c in rng (p | (Seg k))
proof
consider n being set  such that
A33: n in dom p and
A34: p . n = c by A10, A19, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A33;
A35: Seg (k + 1) = dom p by A11, FINSEQ_1:def_3;
then  n <= k + 1 by A33, FINSEQ_1:1;
then  n < k + 1 by A17, A21, A34, XXREAL_0:1;
then A36: n <= k by NAT_1:13;
 1 <= n by A33, A35, FINSEQ_1:1;
then  n in Seg k by A36, FINSEQ_1:1;
then A37: n in dom (p | (Seg k)) by A14, FINSEQ_1:17;
then  (p | (Seg k)) . n = c by A34, FUNCT_1:47;
hence  c in rng (p | (Seg k)) by A37, FUNCT_1:def_3; ::_thesis: verum
end;
assume A38: u <= a ; ::_thesis: contradiction
then  c <> a by A17, A20, A21, A26, A30, ORDERS_2:2;
hence  contradiction by A16, A17, A20, A26, A30, A38, A32, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
hence  ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) by A10, A12, A15; ::_thesis: verum
end;
suppose for c being Element of (LattPOSet L) holds
( not c in X or not c <= b or not c <> b ) ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
then  for u being Element of (LattPOSet L) st u in X & u <> b holds
not u <= b ;
hence  ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) by A10, A18; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
end;
end;
A39: S1[ 0 ]
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = 0 & not X is empty implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
assume that
A40: rng p = X and
A41: len p = 0 ; ::_thesis: ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
 Seg 0 = dom p by A41, FINSEQ_1:def_3;
hence  ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) ) by A40, RELAT_1:42; ::_thesis: verum
end;
A42: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A39, A1);
reconsider X = X as finite Subset of L ;
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
then reconsider X9 = X as finite Subset of (LattPOSet L) ;
consider p being FinSequence such that
A43: rng p = X9 by FINSEQ_1:52;
 dom p = Seg (len p) by FINSEQ_1:def_3;
hence  ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) ) by A42, A43; ::_thesis: verum
end;

Lm2:  for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
proof
defpred S1[ Element of NAT ] means  for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = $1 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) );
let L be finite Lattice; ::_thesis: for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
let X be Subset of L; ::_thesis: ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
percases ( k = 0 or k <> 0 ) ;
supposeA3: k = 0 ; ::_thesis: S1[k + 1]
 for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = 1 implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
assume that
A4: rng p = X and
A5: len p = 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
consider a being set  such that
A6: p . 1 = a ;
A7: dom p = {1} by A5, FINSEQ_1:2, FINSEQ_1:def_3;
then  1 in dom p by TARSKI:def_1;
then A8: a in rng p by A6, FUNCT_1:def_3;
then reconsider a = a as Element of (LattPOSet L) by A4;
 rng p = {a} by A7, A6, FUNCT_1:4;
then  for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b by A4, TARSKI:def_1;
hence  ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) by A4, A8; ::_thesis: verum
end;
hence  S1[k + 1] by A3; ::_thesis: verum
end;
supposeA9: k <> 0 ; ::_thesis: S1[k + 1]
 for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
assume that
A10: rng p = X and
A11: len p = k + 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
set q = p | (Seg k);
set X9 = rng (p | (Seg k));
A12: rng (p | (Seg k)) c= rng p by RELAT_1:70;
 for x being set st x in rng (p | (Seg k)) holds
x in the carrier of (LattPOSet L)
proof
let x be set ; ::_thesis: ( x in rng (p | (Seg k)) implies x in the carrier of (LattPOSet L) )
assume  x in rng (p | (Seg k)) ; ::_thesis: x in the carrier of (LattPOSet L)
then  x in rng p by A12;
hence  x in the carrier of (LattPOSet L) by A10; ::_thesis: verum
end;
then A13: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def_3;
A14: k <= len p by A11, NAT_1:11;
then  ( len (p | (Seg k)) = k & p | (Seg k) <> {} ) by A9, CARD_1:27, FINSEQ_1:17;
then consider a being Element of (LattPOSet L) such that
A15: a in rng (p | (Seg k)) and
A16: for b being Element of (LattPOSet L) st b in rng (p | (Seg k)) & b <> a holds
not a <= b by A2, A13;
consider b being set  such that
A17: p . (k + 1) = b ;
 Seg (k + 1) = dom p by A11, FINSEQ_1:def_3;
then  k + 1 in dom p by FINSEQ_1:4;
then A18: b in rng p by A17, FUNCT_1:def_3;
then reconsider b = b as Element of (LattPOSet L) by A10;
percases ( ex c being Element of (LattPOSet L) st
( c in X & b <= c & c <> b ) or for c being Element of (LattPOSet L) holds
( not c in X or not b <= c or not c <> b ) ) ;
suppose ex c being Element of (LattPOSet L) st
( c in X & b <= c & c <> b ) ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
then consider c being Element of (LattPOSet L) such that
A19: c in X and
A20: b <= c and
A21: c <> b ;
 for u being Element of (LattPOSet L) st u in X & u <> a holds
not a <= u
proof
let u be Element of (LattPOSet L); ::_thesis: ( u in X & u <> a implies not a <= u )
assume that
A22: u in X and
A23: u <> a ; ::_thesis: not a <= u
now__::_thesis:_(_(_u_in_rng_(p_|_(Seg_k))_&_not_a_<=_u_)_or_(_not_u_in_rng_(p_|_(Seg_k))_&_(_a_<=_u_implies_not_a_<=_u_)_)_)
percases ( u in rng (p | (Seg k)) or not u in rng (p | (Seg k)) ) ;
case u in rng (p | (Seg k)) ; ::_thesis: not a <= u
hence  not a <= u by A16, A23; ::_thesis: verum
end;
caseA24: not u in rng (p | (Seg k)) ; ::_thesis: ( a <= u implies not a <= u )
consider n being set  such that
A25: n in dom p and
A26: p . n = u by A10, A22, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A25;
A27: Seg (k + 1) = dom p by A11, FINSEQ_1:def_3;
then A28: n <= k + 1 by A25, FINSEQ_1:1;
A29: 1 <= n by A25, A27, FINSEQ_1:1;
A30: n = k + 1
proof
assume  n <> k + 1 ; ::_thesis: contradiction
then  n < k + 1 by A28, XXREAL_0:1;
then  n <= k by NAT_1:13;
then  n in Seg k by A29, FINSEQ_1:1;
then A31: n in dom (p | (Seg k)) by A14, FINSEQ_1:17;
then  (p | (Seg k)) . n = u by A26, FUNCT_1:47;
hence  contradiction by A24, A31, FUNCT_1:def_3; ::_thesis: verum
end;
A32: c in rng (p | (Seg k))
proof
consider n being set  such that
A33: n in dom p and
A34: p . n = c by A10, A19, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A33;
A35: Seg (k + 1) = dom p by A11, FINSEQ_1:def_3;
then  n <= k + 1 by A33, FINSEQ_1:1;
then  n < k + 1 by A17, A21, A34, XXREAL_0:1;
then A36: n <= k by NAT_1:13;
 1 <= n by A33, A35, FINSEQ_1:1;
then  n in Seg k by A36, FINSEQ_1:1;
then A37: n in dom (p | (Seg k)) by A14, FINSEQ_1:17;
then  (p | (Seg k)) . n = c by A34, FUNCT_1:47;
hence  c in rng (p | (Seg k)) by A37, FUNCT_1:def_3; ::_thesis: verum
end;
assume  a <= u ; ::_thesis: not a <= u
then  c <> a by A17, A20, A21, A26, A30, ORDERS_2:2;
hence  not a <= u by A16, A17, A20, A26, A30, A32, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
hence  not a <= u ; ::_thesis: verum
end;
hence  ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) by A10, A12, A15; ::_thesis: verum
end;
suppose for c being Element of (LattPOSet L) holds
( not c in X or not b <= c or not c <> b ) ; ::_thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
then  for u being Element of (LattPOSet L) st u in X & u <> b holds
not b <= u ;
hence  ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) by A10, A18; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
end;
end;
A38: S1[ 0 ]
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = 0 & not X is empty implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
assume that
A39: rng p = X and
A40: len p = 0 ; ::_thesis: ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
 Seg 0 = dom p by A40, FINSEQ_1:def_3;
hence  ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) ) by A39, RELAT_1:42; ::_thesis: verum
end;
A41: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A38, A1);
reconsider X = X as finite Subset of L ;
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
then reconsider X9 = X as finite Subset of (LattPOSet L) ;
consider p being FinSequence such that
A42: rng p = X9 by FINSEQ_1:52;
 dom p = Seg (len p) by FINSEQ_1:def_3;
hence  ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) ) by A41, A42; ::_thesis: verum
end;

Lm3:  for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
proof
defpred S1[ Element of NAT ] means  for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = $1 & not X is empty holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a;
let L be finite Lattice; ::_thesis: for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
let X be Subset of L; ::_thesis: ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
percases ( k = 0 or k <> 0 ) ;
supposeA3: k = 0 ; ::_thesis: S1[k + 1]
 for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
let p be FinSequence; ::_thesis: ( rng p = X & len p = 1 implies ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that
A4: rng p = X and
A5: len p = 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
consider a being set  such that
A6: p . 1 = a ;
A7: Seg 1 = dom p by A5, FINSEQ_1:def_3;
then  1 in dom p by FINSEQ_1:2, TARSKI:def_1;
then  a in rng p by A6, FUNCT_1:def_3;
then reconsider a = a as Element of (LattPOSet L) by A4;
 rng p = {a} by A7, A6, FINSEQ_1:2, FUNCT_1:4;
then  for b being Element of (LattPOSet L) st b in X holds
b <= a by A4, TARSKI:def_1;
hence  ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ; ::_thesis: verum
end;
hence  S1[k + 1] by A3; ::_thesis: verum
end;
supposeA8: k <> 0 ; ::_thesis: S1[k + 1]
 for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
let p be FinSequence; ::_thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that
A9: rng p = X and
A10: len p = k + 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
consider b being set  such that
A11: p . (k + 1) = b ;
set q = p | (Seg k);
set X9 = rng (p | (Seg k));
 for x being set st x in rng (p | (Seg k)) holds
x in the carrier of (LattPOSet L)
proof
let x be set ; ::_thesis: ( x in rng (p | (Seg k)) implies x in the carrier of (LattPOSet L) )
A12: rng (p | (Seg k)) c= rng p by RELAT_1:70;
assume  x in rng (p | (Seg k)) ; ::_thesis: x in the carrier of (LattPOSet L)
then  x in rng p by A12;
hence  x in the carrier of (LattPOSet L) by A9; ::_thesis: verum
end;
then A13: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def_3;
A14: k <= k + 1 by NAT_1:11;
then  ( len (p | (Seg k)) = k & p | (Seg k) <> {} ) by A8, A10, CARD_1:27, FINSEQ_1:17;
then consider a being Element of (LattPOSet L) such that
A15: for b being Element of (LattPOSet L) st b in rng (p | (Seg k)) holds
b <= a by A2, A13;
 Seg (k + 1) = dom p by A10, FINSEQ_1:def_3;
then  k + 1 in dom p by FINSEQ_1:4;
then  b in rng p by A11, FUNCT_1:def_3;
then reconsider b = b as Element of (LattPOSet L) by A9;
A16: (% b) % = % b by LATTICE3:def_3
.= b by LATTICE3:def_4 ;
set a2 = (% a) "\/" (% b);
(% a) "\/" ((% a) "\/" (% b)) = ((% a) "\/" (% a)) "\/" (% b) by LATTICES:def_5
.= (% a) "\/" (% b) ;
then A17: % a [= (% a) "\/" (% b) by LATTICES:def_3;
(% b) "\/" ((% a) "\/" (% b)) = ((% b) "\/" (% b)) "\/" (% a) by LATTICES:def_5
.= (% b) "\/" (% a) ;
then A18: % b [= (% a) "\/" (% b) by LATTICES:def_3;
A19: (% a) % = % a by LATTICE3:def_3
.= a by LATTICE3:def_4 ;
 for c being Element of (LattPOSet L) st c in X holds
c <= ((% a) "\/" (% b)) %
proof
let c be Element of (LattPOSet L); ::_thesis: ( c in X implies c <= ((% a) "\/" (% b)) % )
assume A20: c in X ; ::_thesis: c <= ((% a) "\/" (% b)) %
percases ( c in rng (p | (Seg k)) or not c in rng (p | (Seg k)) ) ;
suppose c in rng (p | (Seg k)) ; ::_thesis: c <= ((% a) "\/" (% b)) %
then A21: c <= a by A15;
 a <= ((% a) "\/" (% b)) % by A17, A19, LATTICE3:7;
hence  c <= ((% a) "\/" (% b)) % by A21, ORDERS_2:3; ::_thesis: verum
end;
supposeA22: not c in rng (p | (Seg k)) ; ::_thesis: c <= ((% a) "\/" (% b)) %
consider n being set  such that
A23: n in dom p and
A24: c = p . n by A9, A20, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A23;
A25: n in Seg (k + 1) by A10, A23, FINSEQ_1:def_3;
A26: n >= k + 1
proof
assume  not n >= k + 1 ; ::_thesis: contradiction
then A27: n <= k by INT_1:7;
 1 <= n by A25, FINSEQ_1:1;
then A28: n in Seg k by A27, FINSEQ_1:1;
dom (p | (Seg k)) = (dom p) /\ (Seg k) by RELAT_1:61
.= (Seg (k + 1)) /\ (Seg k) by A10, FINSEQ_1:def_3
.= Seg k by FINSEQ_1:7, NAT_1:11 ;
then A29: (p | (Seg k)) . n = c by A24, A28, FUNCT_1:47;
 n in dom (p | (Seg k)) by A10, A14, A28, FINSEQ_1:17;
hence  contradiction by A22, A29, FUNCT_1:def_3; ::_thesis: verum
end;
 n <= k + 1 by A25, FINSEQ_1:1;
then  c = b by A11, A24, A26, XXREAL_0:1;
hence  c <= ((% a) "\/" (% b)) % by A18, A16, LATTICE3:7; ::_thesis: verum
end;
end;
end;
hence  ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
end;
end;
A30: S1[ 0 ]
proof
let L be finite Lattice; ::_thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
let X be Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
let p be FinSequence; ::_thesis: ( rng p = X & len p = 0 & not X is empty implies ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that
A31: rng p = X and
A32: len p = 0 ; ::_thesis: ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
 Seg (len p) = {} by A32;
then  dom p = {} by FINSEQ_1:def_3;
hence  ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ) by A31, RELAT_1:42; ::_thesis: verum
end;
A33: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A30, A1);
reconsider X = X as finite Subset of L ;
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
then reconsider X9 = X as finite Subset of (LattPOSet L) ;
consider p being FinSequence such that
A34: rng p = X9 by FINSEQ_1:52;
 dom p = Seg (len p) by FINSEQ_1:def_3;
hence  ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ) by A33, A34; ::_thesis: verum
end;

Lm4:  for L being finite Lattice ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a
proof
let L be finite Lattice; ::_thesis: ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a
 the carrier of L c= the carrier of L ;
then reconsider L9 = the carrier of L as Subset of L ;
consider a being Element of (LattPOSet L) such that
A1: for b being Element of (LattPOSet L) st b in L9 holds
b <= a by Lm3;
 for b being Element of (LattPOSet L) holds b <= a
proof
let b be Element of (LattPOSet L); ::_thesis: b <= a
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
hence  b <= a by A1; ::_thesis: verum
end;
hence  ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a ; ::_thesis: verum
end;

Lm5:  for L being finite Lattice holds L is complete
proof
let L be finite Lattice; ::_thesis: L is complete
 for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) )
proof
defpred S1[ Element of NAT ] means  for X9 being finite Subset of (LattPOSet L)
for p being FinSequence st rng p = X9 & len p = $1 holds
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) );
let X be Subset of L; ::_thesis: ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) )
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
 for X9 being finite Subset of (LattPOSet L)
for p being FinSequence st rng p = X9 & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) )
proof
let X be finite Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) )
let p be FinSequence; ::_thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) ) )
assume that
A3: rng p = X and
A4: len p = k + 1 ; ::_thesis: ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) )
set q = p | (Seg k);
set X9 = rng (p | (Seg k));
 for x being set st x in rng (p | (Seg k)) holds
x in the carrier of (LattPOSet L)
proof
let x be set ; ::_thesis: ( x in rng (p | (Seg k)) implies x in the carrier of (LattPOSet L) )
A5: rng (p | (Seg k)) c= rng p by RELAT_1:70;
assume  x in rng (p | (Seg k)) ; ::_thesis: x in the carrier of (LattPOSet L)
then  x in rng p by A5;
hence  x in the carrier of (LattPOSet L) by A3; ::_thesis: verum
end;
then A6: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def_3;
A7: k <= k + 1 by NAT_1:11;
then  len (p | (Seg k)) = k by A4, FINSEQ_1:17;
then consider a being Element of (LattPOSet L) such that
A8: for x being Element of (LattPOSet L) st x in rng (p | (Seg k)) holds
a <= x and
A9: for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in rng (p | (Seg k)) holds
x9 <= x ) holds
x9 <= a by A2, A6;
consider b being set  such that
A10: p . (k + 1) = b ;
 Seg (k + 1) = dom p by A4, FINSEQ_1:def_3;
then  k + 1 in dom p by FINSEQ_1:4;
then A11: b in rng p by A10, FUNCT_1:def_3;
then reconsider b = b as Element of (LattPOSet L) by A3;
A12: (% b) % = % b by LATTICE3:def_3
.= b by LATTICE3:def_4 ;
set a2 = (% a) "/\" (% b);
 ((% a) "/\" (% b)) "\/" (% a) = % a by LATTICES:def_8;
then A13: (% a) "/\" (% b) [= % a by LATTICES:def_3;
 ((% a) "/\" (% b)) "\/" (% b) = % b by LATTICES:def_8;
then A14: (% a) "/\" (% b) [= % b by LATTICES:def_3;
A15: (% a) % = % a by LATTICE3:def_3
.= a by LATTICE3:def_4 ;
A16: for x being Element of (LattPOSet L) st x in X holds
((% a) "/\" (% b)) % <= x
proof
let c be Element of (LattPOSet L); ::_thesis: ( c in X implies ((% a) "/\" (% b)) % <= c )
assume A17: c in X ; ::_thesis: ((% a) "/\" (% b)) % <= c
percases ( c in rng (p | (Seg k)) or not c in rng (p | (Seg k)) ) ;
suppose c in rng (p | (Seg k)) ; ::_thesis: ((% a) "/\" (% b)) % <= c
then A18: a <= c by A8;
 ((% a) "/\" (% b)) % <= a by A13, A15, LATTICE3:7;
hence  ((% a) "/\" (% b)) % <= c by A18, ORDERS_2:3; ::_thesis: verum
end;
supposeA19: not c in rng (p | (Seg k)) ; ::_thesis: ((% a) "/\" (% b)) % <= c
consider n being set  such that
A20: n in dom p and
A21: c = p . n by A3, A17, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A20;
A22: n in Seg (k + 1) by A4, A20, FINSEQ_1:def_3;
A23: n >= k + 1
proof
assume  not n >= k + 1 ; ::_thesis: contradiction
then A24: n <= k by INT_1:7;
 1 <= n by A22, FINSEQ_1:1;
then A25: n in Seg k by A24, FINSEQ_1:1;
dom (p | (Seg k)) = (dom p) /\ (Seg k) by RELAT_1:61
.= (Seg (k + 1)) /\ (Seg k) by A4, FINSEQ_1:def_3
.= Seg k by FINSEQ_1:7, NAT_1:11 ;
then A26: (p | (Seg k)) . n = c by A21, A25, FUNCT_1:47;
 n in dom (p | (Seg k)) by A4, A7, A25, FINSEQ_1:17;
hence  contradiction by A19, A26, FUNCT_1:def_3; ::_thesis: verum
end;
 n <= k + 1 by A22, FINSEQ_1:1;
then  c = b by A10, A21, A23, XXREAL_0:1;
hence  ((% a) "/\" (% b)) % <= c by A14, A12, LATTICE3:7; ::_thesis: verum
end;
end;
end;
 for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= ((% a) "/\" (% b)) %
proof
let x9 be Element of (LattPOSet L); ::_thesis: ( ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) implies x9 <= ((% a) "/\" (% b)) % )
A27: (% b) % = % b by LATTICE3:def_3
.= b by LATTICE3:def_4 ;
A28: (% x9) % = % x9 by LATTICE3:def_3
.= x9 by LATTICE3:def_4 ;
assume A29: for x being Element of (LattPOSet L) st x in X holds
x9 <= x ; ::_thesis: x9 <= ((% a) "/\" (% b)) %
 for x being Element of (LattPOSet L) st x in rng (p | (Seg k)) holds
x9 <= x
proof
let x be Element of (LattPOSet L); ::_thesis: ( x in rng (p | (Seg k)) implies x9 <= x )
 rng (p | (Seg k)) c= rng p by RELAT_1:70;
hence  ( x in rng (p | (Seg k)) implies x9 <= x ) by A3, A29; ::_thesis: verum
end;
then A30: x9 <= a by A9;
(% a) % = % a by LATTICE3:def_3
.= a by LATTICE3:def_4 ;
then A31: % x9 [= % a by A30, A28, LATTICE3:7;
 x9 <= b by A3, A11, A29;
then A32: % x9 [= % b by A27, A28, LATTICE3:7;
(% x9) "/\" ((% a) "/\" (% b)) = ((% x9) "/\" (% a)) "/\" (% b) by LATTICES:def_7
.= (% x9) "/\" (% b) by A31, LATTICES:4
.= % x9 by A32, LATTICES:4 ;
then  % x9 [= (% a) "/\" (% b) by LATTICES:4;
hence  x9 <= ((% a) "/\" (% b)) % by A28, LATTICE3:7; ::_thesis: verum
end;
hence  ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) ) by A16; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for X9 being finite Subset of (LattPOSet L)
for p being FinSequence st rng p = X9 & len p = 0 holds
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) )
proof
let X9 be finite Subset of (LattPOSet L); ::_thesis: for p being FinSequence st rng p = X9 & len p = 0 holds
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) )
let p be FinSequence; ::_thesis: ( rng p = X9 & len p = 0 implies ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) ) )
assume that
A33: rng p = X9 and
A34: len p = 0 ; ::_thesis: ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) )
 Seg (len p) = {} by A34;
then A35: dom p = {} by FINSEQ_1:def_3;
 ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) )
proof
consider a being Element of (LattPOSet L) such that
A36: for b being Element of (LattPOSet L) holds b <= a by Lm4;
A37: for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a by A36;
 for x being Element of (LattPOSet L) st x in X9 holds
a <= x by A33, A35, RELAT_1:42;
hence  ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) ) by A37; ::_thesis: verum
end;
hence  ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X9 holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a ) ) ; ::_thesis: verum
end;
then A38: S1[ 0 ] ;
A39: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A38, A1);
reconsider X = X as finite Subset of L ;
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
then reconsider X9 = X as finite Subset of (LattPOSet L) ;
consider p being FinSequence such that
A40: rng p = X9 by FINSEQ_1:52;
 dom p = Seg (len p) by FINSEQ_1:def_3;
then consider a being Element of (LattPOSet L) such that
A41: for x being Element of (LattPOSet L) st x in X9 holds
a <= x and
A42: for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X9 holds
x9 <= x ) holds
x9 <= a by A39, A40;
A43: for b being Element of L st b is_less_than X holds
b [= % a
proof
let b be Element of L; ::_thesis: ( b is_less_than X implies b [= % a )
assume A44: b is_less_than X ; ::_thesis: b [= % a
 for x being Element of (LattPOSet L) st x in X9 holds
b % <= x
proof
let x be Element of (LattPOSet L); ::_thesis: ( x in X9 implies b % <= x )
assume  x in X9 ; ::_thesis: b % <= x
then consider x9 being Element of L such that
A45: x9 = x and
A46: x9 in X ;
 b [= x9 by A44, A46, LATTICE3:def_16;
then  b % <= x9 % by LATTICE3:7;
hence  b % <= x by A45, LATTICE3:def_3; ::_thesis: verum
end;
then A47: b % <= a by A42;
(% a) % = % a by LATTICE3:def_3
.= a by LATTICE3:def_4 ;
hence  b [= % a by A47, LATTICE3:7; ::_thesis: verum
end;
 for x being Element of L st x in X holds
% a [= x
proof
let x be Element of L; ::_thesis: ( x in X implies % a [= x )
A48: (% a) % = % a by LATTICE3:def_3
.= a by LATTICE3:def_4 ;
assume  x in X ; ::_thesis: % a [= x
then consider x9 being Element of (LattPOSet L) such that
A49: ( x9 = x & x9 in X9 ) ;
 ( a <= x9 & x9 = x % ) by A41, A49, LATTICE3:def_3;
hence  % a [= x by A48, LATTICE3:7; ::_thesis: verum
end;
then  % a is_less_than X by LATTICE3:def_16;
hence  ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) by A43; ::_thesis: verum
end;
hence  L is complete by VECTSP_8:def_6; ::_thesis: verum
end;

registration
cluster non empty finite Lattice-like  ->  complete for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is complete by Lm5;
end;

definition
let L be Lattice;
let D be Subset of L;
funcD %  ->  Subset of (LattPOSet L) equals :: LATTICE6:def 1
 {  (d %) where d is Element of L : d in D  }  ;
coherence
  {  (d %) where d is Element of L : d in D  }  is Subset of (LattPOSet L)
proof
set M9 =  {  (d %) where d is Element of L : d in D  }  ;
 for x being set st x in  {  (d %) where d is Element of L : d in D  }  holds
x in the carrier of (LattPOSet L)
proof
let x be set ; ::_thesis: ( x in  {  (d %) where d is Element of L : d in D  }  implies x in the carrier of (LattPOSet L) )
assume  x in  {  (d %) where d is Element of L : d in D  }  ; ::_thesis: x in the carrier of (LattPOSet L)
then  ex x9 being Element of L st
( x = x9 % & x9 in D ) ;
hence  x in the carrier of (LattPOSet L) ; ::_thesis: verum
end;
hence   {  (d %) where d is Element of L : d in D  }  is Subset of (LattPOSet L) by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines % LATTICE6:def_1_:_
 for L being Lattice
for D being Subset of L holds D % =  {  (d %) where d is Element of L : d in D  }  ;

definition
let L be Lattice;
let D be Subset of (LattPOSet L);
func % D ->  Subset of L equals :: LATTICE6:def 2
 {  (% d) where d is Element of (LattPOSet L) : d in D  }  ;
coherence
  {  (% d) where d is Element of (LattPOSet L) : d in D  }  is Subset of L
proof
set M9 =  {  (% d) where d is Element of (LattPOSet L) : d in D  }  ;
 for x being set st x in  {  (% d) where d is Element of (LattPOSet L) : d in D  }  holds
x in the carrier of L
proof
let x be set ; ::_thesis: ( x in  {  (% d) where d is Element of (LattPOSet L) : d in D  }  implies x in the carrier of L )
assume  x in  {  (% d) where d is Element of (LattPOSet L) : d in D  }  ; ::_thesis: x in the carrier of L
then  ex x9 being Element of (LattPOSet L) st
( x = % x9 & x9 in D ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
hence   {  (% d) where d is Element of (LattPOSet L) : d in D  }  is Subset of L by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines % LATTICE6:def_2_:_
 for L being Lattice
for D being Subset of (LattPOSet L) holds % D =  {  (% d) where d is Element of (LattPOSet L) : d in D  }  ;

registration
let L be finite Lattice;
cluster LattPOSet L ->  well_founded ;
coherence
 LattPOSet L is well_founded
proof
let Y be set ; :: according to WELLFND1:def_2,WELLORD1:def_3 ::_thesis: ( not Y c= the carrier of (LattPOSet L) or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of (LattPOSet L) -Seg b1 misses Y ) )
set R = LattPOSet L;
assume that
A1: Y c= the carrier of (LattPOSet L) and
A2: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of (LattPOSet L) -Seg b1 misses Y )
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
then reconsider Y = Y as Subset of L by A1;
consider a being Element of (LattPOSet L) such that
A3: a in Y and
A4: for b being Element of (LattPOSet L) st b in Y & b <> a holds
not b <= a by A2, Lm1;
A5: for x being Element of (LattPOSet L) holds
( not x <> a or not [x,a] in the InternalRel of (LattPOSet L) or not x in Y )
proof
given x being Element of (LattPOSet L) such that A6: x <> a and
A7: [x,a] in the InternalRel of (LattPOSet L) and
A8: x in Y ; ::_thesis: contradiction
 x <= a by A7, ORDERS_2:def_5;
hence  contradiction by A4, A6, A8; ::_thesis: verum
end;
 ( the InternalRel of (LattPOSet L) -Seg a) /\ Y = {}
proof
set z = the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y;
assume A9: ( the InternalRel of (LattPOSet L) -Seg a) /\ Y <> {} ; ::_thesis: contradiction
then  the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y in the InternalRel of (LattPOSet L) -Seg a by XBOOLE_0:def_4;
then A10: ( the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y <> a & [ the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y,a] in the InternalRel of (LattPOSet L) ) by WELLORD1:1;
 the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y in Y by A9, XBOOLE_0:def_4;
hence  contradiction by A1, A5, A10; ::_thesis: verum
end;
then  the InternalRel of (LattPOSet L) -Seg a misses Y by XBOOLE_0:def_7;
hence  ex b1 being set st
( b1 in Y & the InternalRel of (LattPOSet L) -Seg b1 misses Y ) by A3; ::_thesis: verum
end;
end;

Lm6:  for L being finite Lattice holds (LattPOSet L) ~ is well_founded
proof
let L be finite Lattice; ::_thesis: (LattPOSet L) ~ is well_founded
set R = LattPOSet L;
A1: (LattPOSet L) ~ = RelStr(# the carrier of (LattPOSet L),( the InternalRel of (LattPOSet L) ~) #) by LATTICE3:def_5;
 for Y being set st Y c= the carrier of ((LattPOSet L) ~) & Y <> {} holds
ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~) -Seg a misses Y )
proof
let Y be set ; ::_thesis: ( Y c= the carrier of ((LattPOSet L) ~) & Y <> {} implies ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~) -Seg a misses Y ) )
assume that
A2: Y c= the carrier of ((LattPOSet L) ~) and
A3: Y <> {} ; ::_thesis: ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~) -Seg a misses Y )
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
then reconsider Y = Y as Subset of L by A1, A2;
consider a being Element of (LattPOSet L) such that
A4: a in Y and
A5: for b being Element of (LattPOSet L) st b in Y & b <> a holds
not a <= b by A3, Lm2;
reconsider a = a as Element of (LattPOSet L) ;
reconsider a9 = a as Element of ((LattPOSet L) ~) by A1;
A6: for b being Element of ((LattPOSet L) ~) st b in Y & b <> a holds
not b <= a9
proof
let b be Element of ((LattPOSet L) ~); ::_thesis: ( b in Y & b <> a implies not b <= a9 )
reconsider b9 = b as Element of (LattPOSet L) by A1;
assume  ( b in Y & b <> a ) ; ::_thesis: not b <= a9
then A7: not a <= b9 by A5;
 ( a ~ = a9 & b9 ~ = b ) by LATTICE3:def_6;
hence  not b <= a9 by A7, LATTICE3:9; ::_thesis: verum
end;
A8: for x being Element of ((LattPOSet L) ~) holds
( not x <> a or not [x,a] in the InternalRel of ((LattPOSet L) ~) or not x in Y )
proof
given x being Element of ((LattPOSet L) ~) such that A9: x <> a and
A10: [x,a] in the InternalRel of ((LattPOSet L) ~) and
A11: x in Y ; ::_thesis: contradiction
 x <= a9 by A10, ORDERS_2:def_5;
hence  contradiction by A6, A9, A11; ::_thesis: verum
end;
 ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y = {}
proof
set z = the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y;
assume A12: ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y <> {} ; ::_thesis: contradiction
then  the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y in the InternalRel of ((LattPOSet L) ~) -Seg a by XBOOLE_0:def_4;
then A13: ( the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y <> a & [ the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y,a] in the InternalRel of ((LattPOSet L) ~) ) by WELLORD1:1;
 the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y in Y by A12, XBOOLE_0:def_4;
hence  contradiction by A2, A8, A13; ::_thesis: verum
end;
then  the InternalRel of ((LattPOSet L) ~) -Seg a misses Y by XBOOLE_0:def_7;
hence  ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~) -Seg a misses Y ) by A4; ::_thesis: verum
end;
then  the InternalRel of ((LattPOSet L) ~) is_well_founded_in the carrier of ((LattPOSet L) ~) by WELLORD1:def_3;
hence  (LattPOSet L) ~ is well_founded by WELLFND1:def_2; ::_thesis: verum
end;

definition
let L be Lattice;
attrL is noetherian  means :Def3: :: LATTICE6:def 3
 LattPOSet L is well_founded ;
attrL is co-noetherian  means :Def4: :: LATTICE6:def 4
(LattPOSet L) ~ is well_founded ;
end;

:: deftheorem Def3 defines noetherian LATTICE6:def_3_:_
 for L being Lattice holds
( L is noetherian iff LattPOSet L is well_founded );

:: deftheorem Def4 defines co-noetherian LATTICE6:def_4_:_
 for L being Lattice holds
( L is co-noetherian iff (LattPOSet L) ~ is well_founded );

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded complete noetherian for LattStr ;
existence
 ex b1 being Lattice st
( b1 is noetherian & b1 is upper-bounded & b1 is lower-bounded & b1 is complete )
proof
set L = the finite Lattice;
take  the finite Lattice ; ::_thesis: ( the finite Lattice is noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete )
 LattPOSet the finite Lattice is well_founded ;
hence  ( the finite Lattice is noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete ) by Def3; ::_thesis: verum
end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded complete co-noetherian for LattStr ;
existence
 ex b1 being Lattice st
( b1 is co-noetherian & b1 is upper-bounded & b1 is lower-bounded & b1 is complete )
proof
set L = the finite Lattice;
take  the finite Lattice ; ::_thesis: ( the finite Lattice is co-noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete )
 (LattPOSet the finite Lattice) ~ is well_founded by Lm6;
hence  ( the finite Lattice is co-noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete ) by Def4; ::_thesis: verum
end;
end;

theorem :: LATTICE6:1
for L being Lattice holds
( L is noetherian iff L .: is co-noetherian )
proof
let L be Lattice; ::_thesis: ( L is noetherian iff L .: is co-noetherian )
set R = LattPOSet L;
set Ri = (LattPOSet L) ~ ;
A1: now__::_thesis:_(_L_.:_is_co-noetherian_implies_L_is_noetherian_)
A2: (LattPOSet L) ~ = LattPOSet (L .:) by LATTICE3:20;
assume  L .: is co-noetherian ; ::_thesis: L is noetherian
then  ((LattPOSet L) ~) ~ is well_founded by A2, Def4;
then  LattPOSet L is well_founded by LATTICE3:8;
hence  L is noetherian by Def3; ::_thesis: verum
end;
now__::_thesis:_(_L_is_noetherian_implies_L_.:_is_co-noetherian_)
assume  L is noetherian ; ::_thesis: L .: is co-noetherian
then  LattPOSet L is well_founded by Def3;
then A3: ((LattPOSet L) ~) ~ is well_founded by LATTICE3:8;
 (LattPOSet L) ~ = LattPOSet (L .:) by LATTICE3:20;
hence  L .: is co-noetherian by A3, Def4; ::_thesis: verum
end;
hence  ( L is noetherian iff L .: is co-noetherian ) by A1; ::_thesis: verum
end;

Lm7:  for L being finite Lattice holds
( L is noetherian & L is co-noetherian )
proof
let L be finite Lattice; ::_thesis: ( L is noetherian & L is co-noetherian )
 (LattPOSet L) ~ is well_founded by Lm6;
hence  ( L is noetherian & L is co-noetherian ) by Def3, Def4; ::_thesis: verum
end;

registration
cluster non empty finite Lattice-like  ->  noetherian for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is noetherian by Lm7;
cluster non empty finite Lattice-like  ->  co-noetherian for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is co-noetherian by Lm7;
end;

definition
let L be Lattice;
let a, b be Element of L;
preda is-upper-neighbour-of b means :Def5: :: LATTICE6:def 5
( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) );
end;

:: deftheorem Def5 defines is-upper-neighbour-of LATTICE6:def_5_:_
 for L being Lattice
for a, b being Element of L holds
( a is-upper-neighbour-of b iff ( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) ) );

notation
let L be Lattice;
let a, b be Element of L;
synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;
end;

theorem Th2: :: LATTICE6:2
for L being Lattice
for a, b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
proof
let L be Lattice; ::_thesis: for a, b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
let a be Element of L; ::_thesis: for b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
let b, c be Element of L; ::_thesis: ( b <> c implies ( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) ) )
assume A1: b <> c ; ::_thesis: ( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
A2: now__::_thesis:_(_b_is-lower-neighbour-of_a_&_c_is-lower-neighbour-of_a_implies_b_"\/"_c_=_a_)
assume that
A3: b is-lower-neighbour-of a and
A4: c is-lower-neighbour-of a ; ::_thesis: b "\/" c = a
A5: b [= a by A3, Def5;
A6: c [= a by A4, Def5;
A7: not b "\/" c = c
proof
assume  b "\/" c = c ; ::_thesis: contradiction
then  b [= c by LATTICES:def_3;
then  ( c = a or c = b ) by A3, A6, Def5;
hence  contradiction by A1, A4, Def5; ::_thesis: verum
end;
a = a "\/" a
.= (b "\/" a) "\/" a by A5, LATTICES:def_3
.= (b "\/" a) "\/" (c "\/" a) by A6, LATTICES:def_3
.= b "\/" (a "\/" (a "\/" c)) by LATTICES:def_5
.= b "\/" ((a "\/" a) "\/" c) by LATTICES:def_5
.= b "\/" (a "\/" c)
.= (b "\/" c) "\/" a by LATTICES:def_5 ;
then A8: b "\/" c [= a by LATTICES:def_3;
 c [= b "\/" c by LATTICES:5;
hence  b "\/" c = a by A4, A8, A7, Def5; ::_thesis: verum
end;
now__::_thesis:_(_b_is-upper-neighbour-of_a_&_c_is-upper-neighbour-of_a_implies_b_"/\"_c_=_a_)
assume that
A9: b is-upper-neighbour-of a and
A10: c is-upper-neighbour-of a ; ::_thesis: b "/\" c = a
A11: a [= b by A9, Def5;
A12: a [= c by A10, Def5;
A13: not b "/\" c = c
proof
assume  b "/\" c = c ; ::_thesis: contradiction
then  c [= b by LATTICES:4;
then  ( c = a or c = b ) by A9, A12, Def5;
hence  contradiction by A1, A10, Def5; ::_thesis: verum
end;
a = a "/\" a
.= (b "/\" a) "/\" a by A11, LATTICES:4
.= (b "/\" a) "/\" (c "/\" a) by A12, LATTICES:4
.= b "/\" (a "/\" (c "/\" a)) by LATTICES:def_7
.= b "/\" ((a "/\" a) "/\" c) by LATTICES:def_7
.= b "/\" (a "/\" c)
.= (b "/\" c) "/\" a by LATTICES:def_7 ;
then A14: a [= b "/\" c by LATTICES:4;
 b "/\" c [= c by LATTICES:6;
hence  b "/\" c = a by A10, A14, A13, Def5; ::_thesis: verum
end;
hence  ( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) ) by A2; ::_thesis: verum
end;

theorem Th3: :: LATTICE6:3
for L being noetherian Lattice
for a, d being Element of L st a [= d & a <> d holds
ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
proof
let L be noetherian Lattice; ::_thesis: for a, d being Element of L st a [= d & a <> d holds
ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
let a, d be Element of L; ::_thesis: ( a [= d & a <> d implies ex c being Element of L st
( c [= d & c is-upper-neighbour-of a ) )
defpred S1[ Element of (LattPOSet L)] means ( a [= % $1 & a <> % $1 implies ex c being Element of L st
( c [= % $1 & c is-upper-neighbour-of a ) );
A1: % (d %) = d % by LATTICE3:def_4
.= d by LATTICE3:def_3 ;
A2: for x being Element of (LattPOSet L) st ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ) holds
S1[x]
proof
let x be Element of (LattPOSet L); ::_thesis: ( ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ) implies S1[x] )
assume A3: for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ; ::_thesis: S1[x]
 ( a [= % x & a <> % x implies ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) )
proof
A4: (% x) % = % x by LATTICE3:def_3
.= x by LATTICE3:def_4 ;
assume A5: ( a [= % x & a <> % x ) ; ::_thesis: ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a )
percases ( % x is-upper-neighbour-of a or not % x is-upper-neighbour-of a ) ;
suppose % x is-upper-neighbour-of a ; ::_thesis: ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a )
hence  ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) ; ::_thesis: verum
end;
suppose not % x is-upper-neighbour-of a ; ::_thesis: ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a )
then consider c being Element of L such that
A6: a [= c and
A7: c [= % x and
A8: ( not c = % x & not c = a ) by A5, Def5;
 c % <= x by A4, A7, LATTICE3:7;
then A9: [(c %),x] in the InternalRel of (LattPOSet L) by ORDERS_2:def_5;
% (c %) = c % by LATTICE3:def_4
.= c by LATTICE3:def_3 ;
then  ex c9 being Element of L st
( c9 [= c & c9 is-upper-neighbour-of a ) by A3, A6, A8, A9;
hence  ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) by A7, LATTICES:7; ::_thesis: verum
end;
end;
end;
hence  S1[x] ; ::_thesis: verum
end;
A10: LattPOSet L is well_founded by Def3;
A11: for x being Element of (LattPOSet L) holds S1[x] from WELLFND1:sch_3(A2, A10);
assume  ( a [= d & a <> d ) ; ::_thesis: ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
hence  ex c being Element of L st
( c [= d & c is-upper-neighbour-of a ) by A11, A1; ::_thesis: verum
end;

theorem Th4: :: LATTICE6:4
for L being co-noetherian Lattice
for a, d being Element of L st d [= a & a <> d holds
ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )
proof
let L be co-noetherian Lattice; ::_thesis: for a, d being Element of L st d [= a & a <> d holds
ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )
let a, d be Element of L; ::_thesis: ( d [= a & a <> d implies ex c being Element of L st
( d [= c & c is-lower-neighbour-of a ) )
defpred S1[ Element of ((LattPOSet L) ~)] means ( % (~ $1) [= a & a <> % (~ $1) implies ex c being Element of L st
( % (~ $1) [= c & c is-lower-neighbour-of a ) );
A1: % (~ ((d %) ~)) = ~ ((d %) ~) by LATTICE3:def_4
.= (d %) ~ by LATTICE3:def_7
.= d % by LATTICE3:def_6
.= d by LATTICE3:def_3 ;
A2: for x being Element of ((LattPOSet L) ~) st ( for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ) holds
S1[x]
proof
let x be Element of ((LattPOSet L) ~); ::_thesis: ( ( for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ) implies S1[x] )
assume A3: for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ; ::_thesis: S1[x]
 ( % (~ x) [= a & a <> % (~ x) implies ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a ) )
proof
A4: (~ x) ~ = ~ x by LATTICE3:def_6
.= x by LATTICE3:def_7 ;
A5: (% (~ x)) % = % (~ x) by LATTICE3:def_3
.= ~ x by LATTICE3:def_4 ;
assume A6: ( % (~ x) [= a & a <> % (~ x) ) ; ::_thesis: ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a )
percases ( % (~ x) is-lower-neighbour-of a or not % (~ x) is-lower-neighbour-of a ) ;
suppose % (~ x) is-lower-neighbour-of a ; ::_thesis: ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a )
hence  ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a ) ; ::_thesis: verum
end;
suppose not % (~ x) is-lower-neighbour-of a ; ::_thesis: ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a )
then consider c being Element of L such that
A7: % (~ x) [= c and
A8: ( c [= a & not c = a & not c = % (~ x) ) by A6, Def5;
A9: % (~ ((c %) ~)) = ~ ((c %) ~) by LATTICE3:def_4
.= (c %) ~ by LATTICE3:def_7
.= c % by LATTICE3:def_6
.= c by LATTICE3:def_3 ;
 ~ x <= c % by A5, A7, LATTICE3:7;
then  (c %) ~ <= x by A4, LATTICE3:9;
then  [((c %) ~),x] in the InternalRel of ((LattPOSet L) ~) by ORDERS_2:def_5;
then  ex c9 being Element of L st
( % (~ ((c %) ~)) [= c9 & c9 is-lower-neighbour-of a ) by A3, A8, A9;
hence  ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a ) by A7, A9, LATTICES:7; ::_thesis: verum
end;
end;
end;
hence  S1[x] ; ::_thesis: verum
end;
A10: (LattPOSet L) ~ is well_founded by Def4;
A11: for x being Element of ((LattPOSet L) ~) holds S1[x] from WELLFND1:sch_3(A2, A10);
assume  ( d [= a & a <> d ) ; ::_thesis: ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )
hence  ex c being Element of L st
( d [= c & c is-lower-neighbour-of a ) by A11, A1; ::_thesis: verum
end;

theorem Th5: :: LATTICE6:5
for L being upper-bounded Lattice
for b being Element of L holds not b is-upper-neighbour-of Top L
proof
let L be upper-bounded Lattice; ::_thesis: for b being Element of L holds not b is-upper-neighbour-of Top L
given b being Element of L such that A1: b is-upper-neighbour-of Top L ; ::_thesis: contradiction
A2: b [= Top L by LATTICES:19;
 ( Top L [= b & Top L <> b ) by A1, Def5;
hence  contradiction by A2, LATTICES:8; ::_thesis: verum
end;

theorem Th6: :: LATTICE6:6
for L being upper-bounded noetherian Lattice
for a being Element of L holds
( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a )
proof
let L be upper-bounded noetherian Lattice; ::_thesis: for a being Element of L holds
( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a )
let a be Element of L; ::_thesis: ( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a )
now__::_thesis:_(_(_for_b_being_Element_of_L_holds_not_b_is-upper-neighbour-of_a_)_implies_a_=_Top_L_)
assume A1: for b being Element of L holds not b is-upper-neighbour-of a ; ::_thesis: a = Top L
 for b being Element of L holds
( a "\/" b = a & b "\/" a = a )
proof
let b be Element of L; ::_thesis: ( a "\/" b = a & b "\/" a = a )
consider c being Element of L such that
A2: c = a "\/" b ;
A3: a [= c by A2, LATTICES:5;
percases ( a <> c or a = c ) ;
suppose a <> c ; ::_thesis: ( a "\/" b = a & b "\/" a = a )
then  ex d being Element of L st
( d [= c & d is-upper-neighbour-of a ) by A3, Th3;
hence  ( a "\/" b = a & b "\/" a = a ) by A1; ::_thesis: verum
end;
suppose a = c ; ::_thesis: ( a "\/" b = a & b "\/" a = a )
hence  ( a "\/" b = a & b "\/" a = a ) by A2; ::_thesis: verum
end;
end;
end;
hence  a = Top L by LATTICES:def_17; ::_thesis: verum
end;
hence  ( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a ) by Th5; ::_thesis: verum
end;

theorem Th7: :: LATTICE6:7
for L being lower-bounded Lattice
for b being Element of L holds not b is-lower-neighbour-of Bottom L
proof
let L be lower-bounded Lattice; ::_thesis: for b being Element of L holds not b is-lower-neighbour-of Bottom L
given b being Element of L such that A1: b is-lower-neighbour-of Bottom L ; ::_thesis: contradiction
A2: Bottom L [= b by LATTICES:16;
 ( b [= Bottom L & b <> Bottom L ) by A1, Def5;
hence  contradiction by A2, LATTICES:8; ::_thesis: verum
end;

theorem Th8: :: LATTICE6:8
for L being lower-bounded co-noetherian Lattice
for a being Element of L holds
( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )
proof
let L be lower-bounded co-noetherian Lattice; ::_thesis: for a being Element of L holds
( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )
let a be Element of L; ::_thesis: ( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )
now__::_thesis:_(_(_for_b_being_Element_of_L_holds_not_b_is-lower-neighbour-of_a_)_implies_a_=_Bottom_L_)
assume A1: for b being Element of L holds not b is-lower-neighbour-of a ; ::_thesis: a = Bottom L
 for b being Element of L holds
( a "/\" b = a & b "/\" a = a )
proof
let b be Element of L; ::_thesis: ( a "/\" b = a & b "/\" a = a )
consider c being Element of L such that
A2: c = a "/\" b ;
A3: c [= a by A2, LATTICES:6;
percases ( a <> c or a = c ) ;
suppose a <> c ; ::_thesis: ( a "/\" b = a & b "/\" a = a )
then  ex d being Element of L st
( c [= d & d is-lower-neighbour-of a ) by A3, Th4;
hence  ( a "/\" b = a & b "/\" a = a ) by A1; ::_thesis: verum
end;
suppose a = c ; ::_thesis: ( a "/\" b = a & b "/\" a = a )
hence  ( a "/\" b = a & b "/\" a = a ) by A2; ::_thesis: verum
end;
end;
end;
hence  a = Bottom L by LATTICES:def_16; ::_thesis: verum
end;
hence  ( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a ) by Th7; ::_thesis: verum
end;

definition
let L be complete Lattice;
let a be Element of L;
funca *'  ->  Element of L equals :: LATTICE6:def 6
 "/\" ( {  d where d is Element of L : ( a [= d & d <> a )  }  ,L);
correctness
coherence
"/\" ( {  d where d is Element of L : ( a [= d & d <> a )  }  ,L) is Element of L;
;
func *' a ->  Element of L equals :: LATTICE6:def 7
 "\/" ( {  d where d is Element of L : ( d [= a & d <> a )  }  ,L);
correctness
coherence
"\/" ( {  d where d is Element of L : ( d [= a & d <> a )  }  ,L) is Element of L;
;
end;

:: deftheorem  defines *' LATTICE6:def_6_:_
 for L being complete Lattice
for a being Element of L holds a *' = "/\" ( {  d where d is Element of L : ( a [= d & d <> a )  }  ,L);

:: deftheorem  defines *' LATTICE6:def_7_:_
 for L being complete Lattice
for a being Element of L holds *' a = "\/" ( {  d where d is Element of L : ( d [= a & d <> a )  }  ,L);

definition
let L be complete Lattice;
let a be Element of L;
attra is completely-meet-irreducible  means :Def8: :: LATTICE6:def 8
a *' <> a;
attra is completely-join-irreducible  means :Def9: :: LATTICE6:def 9
 *' a <> a;
end;

:: deftheorem Def8 defines completely-meet-irreducible LATTICE6:def_8_:_
 for L being complete Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff a *' <> a );

:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def_9_:_
 for L being complete Lattice
for a being Element of L holds
( a is completely-join-irreducible iff *' a <> a );

theorem Th9: :: LATTICE6:9
for L being complete Lattice
for a being Element of L holds
( a [= a *' & *' a [= a )
proof
let L be complete Lattice; ::_thesis: for a being Element of L holds
( a [= a *' & *' a [= a )
let a be Element of L; ::_thesis: ( a [= a *' & *' a [= a )
set X =  {  d where d is Element of L : ( a [= d & d <> a )  }  ;
 for q being Element of L st q in  {  d where d is Element of L : ( a [= d & d <> a )  }  holds
a [= q
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( a [= d & d <> a )  }  implies a [= q )
assume  q in  {  d where d is Element of L : ( a [= d & d <> a )  }  ; ::_thesis: a [= q
then  ex q9 being Element of L st
( q9 = q & a [= q9 & q9 <> a ) ;
hence  a [= q ; ::_thesis: verum
end;
then A1: a is_less_than  {  d where d is Element of L : ( a [= d & d <> a )  }  by LATTICE3:def_16;
set X =  {  d where d is Element of L : ( d [= a & d <> a )  }  ;
 for q being Element of L st q in  {  d where d is Element of L : ( d [= a & d <> a )  }  holds
q [= a
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( d [= a & d <> a )  }  implies q [= a )
assume  q in  {  d where d is Element of L : ( d [= a & d <> a )  }  ; ::_thesis: q [= a
then  ex q9 being Element of L st
( q9 = q & q9 [= a & q9 <> a ) ;
hence  q [= a ; ::_thesis: verum
end;
then   {  d where d is Element of L : ( d [= a & d <> a )  }  is_less_than a by LATTICE3:def_17;
hence  ( a [= a *' & *' a [= a ) by A1, LATTICE3:34, LATTICE3:def_21; ::_thesis: verum
end;

theorem :: LATTICE6:10
for L being complete Lattice holds
( (Top L) *' = Top L & (Top L) % is meet-irreducible )
proof
let L be complete Lattice; ::_thesis: ( (Top L) *' = Top L & (Top L) % is meet-irreducible )
set X =  {  d where d is Element of L : ( Top L [= d & d <> Top L )  }  ;
A1:  {  d where d is Element of L : ( Top L [= d & d <> Top L )  }  = {}
proof
assume   {  d where d is Element of L : ( Top L [= d & d <> Top L )  }  <> {} ; ::_thesis: contradiction
then reconsider X =  {  d where d is Element of L : ( Top L [= d & d <> Top L )  }  as non empty set ;
set x = the Element of X;
 the Element of X in X ;
then consider x9 being Element of L such that
 x9 = the Element of X and
A2: ( Top L [= x9 & x9 <> Top L ) ;
 x9 [= Top L by LATTICES:19;
hence  contradiction by A2, LATTICES:8; ::_thesis: verum
end;
A3: for b being Element of L st b is_less_than {} holds
b [= Top L by LATTICES:19;
 for q being Element of L st q in {} holds
Top L [= q ;
then A4: Top L is_less_than {} by LATTICE3:def_16;
Top (LattPOSet L) = "/\" ({},(LattPOSet L)) by YELLOW_0:def_12
.= "/\" ({},L) by YELLOW_0:29
.= Top L by A4, A3, LATTICE3:34 ;
then  (Top L) % = Top (LattPOSet L) by LATTICE3:def_3;
hence  ( (Top L) *' = Top L & (Top L) % is meet-irreducible ) by A1, A4, A3, LATTICE3:34, WAYBEL_6:10; ::_thesis: verum
end;

theorem :: LATTICE6:11
for L being complete Lattice holds
( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )
proof
let L be complete Lattice; ::_thesis: ( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )
set X =  {  d where d is Element of L : ( d [= Bottom L & d <> Bottom L )  }  ;
A1:  {  d where d is Element of L : ( d [= Bottom L & d <> Bottom L )  }  = {}
proof
assume   {  d where d is Element of L : ( d [= Bottom L & d <> Bottom L )  }  <> {} ; ::_thesis: contradiction
then reconsider X =  {  d where d is Element of L : ( d [= Bottom L & d <> Bottom L )  }  as non empty set ;
set x = the Element of X;
 the Element of X in X ;
then consider x9 being Element of L such that
 x9 = the Element of X and
A2: ( x9 [= Bottom L & x9 <> Bottom L ) ;
 Bottom L [= x9 by LATTICES:16;
hence  contradiction by A2, LATTICES:8; ::_thesis: verum
end;
A3: for b being Element of L st b is_greater_than {} holds
Bottom L [= b by LATTICES:16;
A4: for x, y being Element of (LattPOSet L) holds
( not Bottom (LattPOSet L) = x "\/" y or x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) )
proof
reconsider L9 = LattPOSet L as non empty antisymmetric lower-bounded RelStr ;
let x, y be Element of (LattPOSet L); ::_thesis: ( not Bottom (LattPOSet L) = x "\/" y or x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) )
reconsider x9 = x as Element of L9 ;
reconsider y9 = y as Element of L9 ;
assume  Bottom (LattPOSet L) = x "\/" y ; ::_thesis: ( x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) )
then A5: ( Bottom (LattPOSet L) >= x & Bottom (LattPOSet L) >= y ) by YELLOW_0:22;
 ( x9 >= Bottom L9 or y9 >= Bottom L9 ) by YELLOW_0:44;
hence  ( x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) ) by A5, ORDERS_2:2; ::_thesis: verum
end;
 for q being Element of L st q in {} holds
q [= Bottom L ;
then A6: Bottom L is_greater_than {} by LATTICE3:def_17;
Bottom (LattPOSet L) = "\/" ({},(LattPOSet L)) by YELLOW_0:def_11
.= "\/" ({},L) by YELLOW_0:29
.= Bottom L by A6, A3, LATTICE3:def_21 ;
then  (Bottom L) % = Bottom (LattPOSet L) by LATTICE3:def_3;
hence  ( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible ) by A1, A6, A3, A4, LATTICE3:def_21, WAYBEL_6:def_3; ::_thesis: verum
end;

theorem Th12: :: LATTICE6:12
for L being complete Lattice
for a being Element of L st a is completely-meet-irreducible holds
( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )
proof
let L be complete Lattice; ::_thesis: for a being Element of L st a is completely-meet-irreducible holds
( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )
let a be Element of L; ::_thesis: ( a is completely-meet-irreducible implies ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) ) )
set X =  {  x where x is Element of L : ( a [= x & x <> a )  }  ;
 for c being Element of L st a [= c & c [= a *' & not c = a holds
c = a *'
proof
let c be Element of L; ::_thesis: ( a [= c & c [= a *' & not c = a implies c = a *' )
assume that
A1: a [= c and
A2: c [= a *' ; ::_thesis: ( c = a or c = a *' )
assume  c <> a ; ::_thesis: c = a *'
then  c in  {  x where x is Element of L : ( a [= x & x <> a )  }  by A1;
then  a *' [= c by LATTICE3:38;
hence  c = a *' by A2, LATTICES:8; ::_thesis: verum
end;
then A3: for c being Element of L st a [= c & c [= a *' & not c = a *' holds
c = a ;
assume  a is completely-meet-irreducible ; ::_thesis: ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )
then A4: a *' <> a by Def8;
A5: for c being Element of L st c is-upper-neighbour-of a holds
c = a *'
proof
let c be Element of L; ::_thesis: ( c is-upper-neighbour-of a implies c = a *' )
assume A6: c is-upper-neighbour-of a ; ::_thesis: c = a *'
then  ( a <> c & a [= c ) by Def5;
then  c in  {  x where x is Element of L : ( a [= x & x <> a )  }  ;
then A7: a *' [= c by LATTICE3:38;
 a [= a *' by Th9;
hence  c = a *' by A4, A6, A7, Def5; ::_thesis: verum
end;
 a [= a *' by Th9;
hence  ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) ) by A4, A3, A5, Def5; ::_thesis: verum
end;

theorem Th13: :: LATTICE6:13
for L being complete Lattice
for a being Element of L st a is completely-join-irreducible holds
( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )
proof
let L be complete Lattice; ::_thesis: for a being Element of L st a is completely-join-irreducible holds
( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )
let a be Element of L; ::_thesis: ( a is completely-join-irreducible implies ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) ) )
set X =  {  x where x is Element of L : ( x [= a & x <> a )  }  ;
A1: for c being Element of L st *' a [= c & c [= a & not c = a holds
c = *' a
proof
let c be Element of L; ::_thesis: ( *' a [= c & c [= a & not c = a implies c = *' a )
assume that
A2: *' a [= c and
A3: c [= a ; ::_thesis: ( c = a or c = *' a )
assume  c <> a ; ::_thesis: c = *' a
then  c in  {  x where x is Element of L : ( x [= a & x <> a )  }  by A3;
then  c [= *' a by LATTICE3:38;
hence  c = *' a by A2, LATTICES:8; ::_thesis: verum
end;
assume  a is completely-join-irreducible ; ::_thesis: ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )
then A4: *' a <> a by Def9;
A5: for c being Element of L st c is-lower-neighbour-of a holds
c = *' a
proof
let c be Element of L; ::_thesis: ( c is-lower-neighbour-of a implies c = *' a )
assume A6: c is-lower-neighbour-of a ; ::_thesis: c = *' a
then  ( a <> c & c [= a ) by Def5;
then  c in  {  x where x is Element of L : ( x [= a & x <> a )  }  ;
then A7: c [= *' a by LATTICE3:38;
 *' a [= a by Th9;
hence  c = *' a by A4, A6, A7, Def5; ::_thesis: verum
end;
 *' a [= a by Th9;
hence  ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) ) by A4, A1, A5, Def5; ::_thesis: verum
end;

theorem Th14: :: LATTICE6:14
for L being complete noetherian Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) )
proof
let L be complete noetherian Lattice; ::_thesis: for a being Element of L holds
( a is completely-meet-irreducible iff ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) )
let a be Element of L; ::_thesis: ( a is completely-meet-irreducible iff ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) )
set X =  {  x where x is Element of L : ( a [= x & x <> a )  }  ;
hereby  ::_thesis: ( ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) implies a is completely-meet-irreducible )
assume  a is completely-meet-irreducible ; ::_thesis: ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) )
then  ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) ) by Th12;
hence  ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) ; ::_thesis: verum
end;
given b being Element of L such that A1: b is-upper-neighbour-of a and
A2: for c being Element of L st c is-upper-neighbour-of a holds
c = b ; ::_thesis: a is completely-meet-irreducible
A3: a <> b by A1, Def5;
 for q being Element of L st q in  {  x where x is Element of L : ( a [= x & x <> a )  }  holds
b [= q
proof
let q be Element of L; ::_thesis: ( q in  {  x where x is Element of L : ( a [= x & x <> a )  }  implies b [= q )
assume  q in  {  x where x is Element of L : ( a [= x & x <> a )  }  ; ::_thesis: b [= q
then  ex q9 being Element of L st
( q9 = q & a [= q9 & q9 <> a ) ;
then  ex c being Element of L st
( c [= q & c is-upper-neighbour-of a ) by Th3;
hence  b [= q by A2; ::_thesis: verum
end;
then A4: b is_less_than  {  x where x is Element of L : ( a [= x & x <> a )  }  by LATTICE3:def_16;
 a [= b by A1, Def5;
then  b in  {  x where x is Element of L : ( a [= x & x <> a )  }  by A3;
hence  a <> a *' by A3, A4, LATTICE3:41; :: according to LATTICE6:def_8 ::_thesis: verum
end;

theorem Th15: :: LATTICE6:15
for L being complete co-noetherian Lattice
for a being Element of L holds
( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )
proof
let L be complete co-noetherian Lattice; ::_thesis: for a being Element of L holds
( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )
let a be Element of L; ::_thesis: ( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )
set X =  {  x where x is Element of L : ( x [= a & x <> a )  }  ;
A1: now__::_thesis:_(_ex_b_being_Element_of_L_st_
(_b_is-lower-neighbour-of_a_&_(_for_c_being_Element_of_L_st_c_is-lower-neighbour-of_a_holds_
c_=_b_)_)_implies_a_is_completely-join-irreducible_)
given b being Element of L such that A2: b is-lower-neighbour-of a and
A3: for c being Element of L st c is-lower-neighbour-of a holds
c = b ; ::_thesis: a is completely-join-irreducible
A4: a <> b by A2, Def5;
 for q being Element of L st q in  {  x where x is Element of L : ( x [= a & x <> a )  }  holds
q [= b
proof
let q be Element of L; ::_thesis: ( q in  {  x where x is Element of L : ( x [= a & x <> a )  }  implies q [= b )
assume  q in  {  x where x is Element of L : ( x [= a & x <> a )  }  ; ::_thesis: q [= b
then  ex q9 being Element of L st
( q9 = q & q9 [= a & q9 <> a ) ;
then  ex c being Element of L st
( q [= c & c is-lower-neighbour-of a ) by Th4;
hence  q [= b by A3; ::_thesis: verum
end;
then A5: b is_greater_than  {  x where x is Element of L : ( x [= a & x <> a )  }  by LATTICE3:def_17;
 b [= a by A2, Def5;
then  b in  {  x where x is Element of L : ( x [= a & x <> a )  }  by A4;
then  a <> *' a by A4, A5, LATTICE3:40;
hence  a is completely-join-irreducible by Def9; ::_thesis: verum
end;
now__::_thesis:_(_a_is_completely-join-irreducible_implies_ex_b_being_Element_of_L_st_
(_b_is-lower-neighbour-of_a_&_(_for_c_being_Element_of_L_st_c_is-lower-neighbour-of_a_holds_
c_=_b_)_)_)
assume  a is completely-join-irreducible ; ::_thesis: ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) )
then  ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) ) by Th13;
hence  ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) ; ::_thesis: verum
end;
hence  ( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) ) by A1; ::_thesis: verum
end;

theorem Th16: :: LATTICE6:16
for L being complete Lattice
for a being Element of L st a is completely-meet-irreducible holds
a % is meet-irreducible
proof
let L be complete Lattice; ::_thesis: for a being Element of L st a is completely-meet-irreducible holds
a % is meet-irreducible
let a be Element of L; ::_thesis: ( a is completely-meet-irreducible implies a % is meet-irreducible )
set X =  {  d where d is Element of L : ( a [= d & d <> a )  }  ;
assume  a is completely-meet-irreducible ; ::_thesis: a % is meet-irreducible
then A1: a <> a *' by Def8;
 for x, y being Element of (LattPOSet L) holds
( not a % = x "/\" y or x = a % or y = a % )
proof
 a [= a *' by Th9;
then A2: a % <= (a *') % by LATTICE3:7;
A3: % (a %) = a % by LATTICE3:def_4;
A4: ( a = a % & a *' = (a *') % ) by LATTICE3:def_3;
A5: a *' is_less_than  {  d where d is Element of L : ( a [= d & d <> a )  }  by LATTICE3:34;
let x, y be Element of (LattPOSet L); ::_thesis: ( not a % = x "/\" y or x = a % or y = a % )
A6: a = a % by LATTICE3:def_3
.= % (a %) by LATTICE3:def_4 ;
A7: x = % x by LATTICE3:def_4
.= (% x) % by LATTICE3:def_3 ;
assume A8: a % = x "/\" y ; ::_thesis: ( x = a % or y = a % )
then  a % <= x by YELLOW_0:23;
then A9: a [= % x by A7, LATTICE3:7;
assume that
A10: x <> a % and
A11: y <> a % ; ::_thesis: contradiction
A12: y = % y by LATTICE3:def_4
.= (% y) % by LATTICE3:def_3 ;
 a % <= y by A8, YELLOW_0:23;
then A13: a [= % y by A12, LATTICE3:7;
 y = % y by LATTICE3:def_4;
then  % y in  {  d where d is Element of L : ( a [= d & d <> a )  }  by A6, A13, A3, A11;
then  a *' [= % y by A5, LATTICE3:def_16;
then A14: (a *') % <= (% y) % by LATTICE3:7;
 x = % x by LATTICE3:def_4;
then  % x in  {  d where d is Element of L : ( a [= d & d <> a )  }  by A6, A9, A3, A10;
then  a *' [= % x by A5, LATTICE3:def_16;
then  (a *') % <= (% x) % by LATTICE3:7;
then  (a *') % <= a % by A8, A12, A7, A14, YELLOW_0:23;
hence  contradiction by A1, A2, A4, ORDERS_2:2; ::_thesis: verum
end;
hence  a % is meet-irreducible by WAYBEL_6:def_2; ::_thesis: verum
end;

Lm8:  for L being Lattice
for a, b being Element of L holds
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
proof
let L be Lattice; ::_thesis: for a, b being Element of L holds
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
let a, b be Element of L; ::_thesis: ( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
consider c being Element of L such that
A1: c = a "/\" b ;
A2: for d being Element of (LattPOSet L) st d <= a % & d <= b % holds
c % >= d
proof
let d be Element of (LattPOSet L); ::_thesis: ( d <= a % & d <= b % implies c % >= d )
assume that
A3: d <= a % and
A4: d <= b % ; ::_thesis: c % >= d
A5: (% d) % = % d by LATTICE3:def_3
.= d by LATTICE3:def_4 ;
then A6: % d [= a by A3, LATTICE3:7;
A7: % d [= b by A4, A5, LATTICE3:7;
(% d) "/\" c = ((% d) "/\" a) "/\" b by A1, LATTICES:def_7
.= (% d) "/\" b by A6, LATTICES:4
.= % d by A7, LATTICES:4 ;
then  % d [= c by LATTICES:4;
hence  c % >= d by A5, LATTICE3:7; ::_thesis: verum
end;
 c [= b by A1, LATTICES:6;
then A8: c % <= b % by LATTICE3:7;
 c [= a by A1, LATTICES:6;
then  c % <= a % by LATTICE3:7;
then A9: c % = (a %) "/\" (b %) by A8, A2, YELLOW_0:23;
consider c being Element of L such that
A10: c = a "\/" b ;
A11: for d being Element of (LattPOSet L) st a % <= d & b % <= d holds
d >= c %
proof
let d be Element of (LattPOSet L); ::_thesis: ( a % <= d & b % <= d implies d >= c % )
assume that
A12: a % <= d and
A13: b % <= d ; ::_thesis: d >= c %
A14: (% d) % = % d by LATTICE3:def_3
.= d by LATTICE3:def_4 ;
then A15: a [= % d by A12, LATTICE3:7;
A16: b [= % d by A13, A14, LATTICE3:7;
(% d) "\/" c = ((% d) "\/" a) "\/" b by A10, LATTICES:def_5
.= (% d) "\/" b by A15, LATTICES:def_3
.= % d by A16, LATTICES:def_3 ;
then  c [= % d by LATTICES:def_3;
hence  d >= c % by A14, LATTICE3:7; ::_thesis: verum
end;
 b [= c by A10, LATTICES:5;
then A17: b % <= c % by LATTICE3:7;
 a [= c by A10, LATTICES:5;
then  a % <= c % by LATTICE3:7;
then  c % = (a %) "\/" (b %) by A17, A11, YELLOW_0:22;
hence  ( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) ) by A1, A9, A10, LATTICE3:def_3; ::_thesis: verum
end;

theorem Th17: :: LATTICE6:17
for L being complete noetherian Lattice
for a being Element of L st a <> Top L holds
( a is completely-meet-irreducible iff a % is meet-irreducible )
proof
let L be complete noetherian Lattice; ::_thesis: for a being Element of L st a <> Top L holds
( a is completely-meet-irreducible iff a % is meet-irreducible )
let a be Element of L; ::_thesis: ( a <> Top L implies ( a is completely-meet-irreducible iff a % is meet-irreducible ) )
assume  a <> Top L ; ::_thesis: ( a is completely-meet-irreducible iff a % is meet-irreducible )
then consider b being Element of L such that
A1: b is-upper-neighbour-of a by Th6;
A2: b <> a by A1, Def5;
now__::_thesis:_(_a_%_is_meet-irreducible_implies_a_is_completely-meet-irreducible_)
assume A3: a % is meet-irreducible ; ::_thesis: a is completely-meet-irreducible
 for d being Element of L st d is-upper-neighbour-of a holds
d = b
proof
let d be Element of L; ::_thesis: ( d is-upper-neighbour-of a implies d = b )
A4: a % = a by LATTICE3:def_3;
A5: ( d % = d & b % = b ) by LATTICE3:def_3;
assume A6: d is-upper-neighbour-of a ; ::_thesis: d = b
then A7: d <> a by Def5;
assume  d <> b ; ::_thesis: contradiction
then  a = d "/\" b by A1, A6, Th2;
then  a % = (d %) "/\" (b %) by A4, Lm8;
hence  contradiction by A2, A3, A7, A4, A5, WAYBEL_6:def_2; ::_thesis: verum
end;
hence  a is completely-meet-irreducible by A1, Th14; ::_thesis: verum
end;
hence  ( a is completely-meet-irreducible iff a % is meet-irreducible ) by Th16; ::_thesis: verum
end;

theorem Th18: :: LATTICE6:18
for L being complete Lattice
for a being Element of L st a is completely-join-irreducible holds
a % is join-irreducible
proof
let L be complete Lattice; ::_thesis: for a being Element of L st a is completely-join-irreducible holds
a % is join-irreducible
let a be Element of L; ::_thesis: ( a is completely-join-irreducible implies a % is join-irreducible )
set X =  {  d where d is Element of L : ( d [= a & d <> a )  }  ;
assume  a is completely-join-irreducible ; ::_thesis: a % is join-irreducible
then A1: a <> *' a by Def9;
 for x, y being Element of (LattPOSet L) holds
( not a % = x "\/" y or x = a % or y = a % )
proof
 *' a [= a by Th9;
then A2: a % >= (*' a) % by LATTICE3:7;
A3: % (a %) = a % by LATTICE3:def_4;
A4: ( a = a % & *' a = (*' a) % ) by LATTICE3:def_3;
A5:  {  d where d is Element of L : ( d [= a & d <> a )  }  is_less_than *' a by LATTICE3:def_21;
let x, y be Element of (LattPOSet L); ::_thesis: ( not a % = x "\/" y or x = a % or y = a % )
A6: a = a % by LATTICE3:def_3
.= % (a %) by LATTICE3:def_4 ;
A7: x = % x by LATTICE3:def_4
.= (% x) % by LATTICE3:def_3 ;
assume A8: a % = x "\/" y ; ::_thesis: ( x = a % or y = a % )
then  x <= a % by YELLOW_0:22;
then A9: % x [= a by A7, LATTICE3:7;
assume that
A10: x <> a % and
A11: y <> a % ; ::_thesis: contradiction
A12: y = % y by LATTICE3:def_4
.= (% y) % by LATTICE3:def_3 ;
 y <= a % by A8, YELLOW_0:22;
then A13: % y [= a by A12, LATTICE3:7;
 y = % y by LATTICE3:def_4;
then  % y in  {  d where d is Element of L : ( d [= a & d <> a )  }  by A6, A13, A3, A11;
then  % y [= *' a by A5, LATTICE3:def_17;
then A14: (*' a) % >= y by A12, LATTICE3:7;
 x = % x by LATTICE3:def_4;
then  % x in  {  d where d is Element of L : ( d [= a & d <> a )  }  by A6, A9, A3, A10;
then  % x [= *' a by A5, LATTICE3:def_17;
then  (*' a) % >= x by A7, LATTICE3:7;
then  (*' a) % >= a % by A8, A14, YELLOW_0:22;
hence  contradiction by A1, A2, A4, ORDERS_2:2; ::_thesis: verum
end;
hence  a % is join-irreducible by WAYBEL_6:def_3; ::_thesis: verum
end;

theorem Th19: :: LATTICE6:19
for L being complete co-noetherian Lattice
for a being Element of L st a <> Bottom L holds
( a is completely-join-irreducible iff a % is join-irreducible )
proof
let L be complete co-noetherian Lattice; ::_thesis: for a being Element of L st a <> Bottom L holds
( a is completely-join-irreducible iff a % is join-irreducible )
let a be Element of L; ::_thesis: ( a <> Bottom L implies ( a is completely-join-irreducible iff a % is join-irreducible ) )
assume  a <> Bottom L ; ::_thesis: ( a is completely-join-irreducible iff a % is join-irreducible )
then consider b being Element of L such that
A1: b is-lower-neighbour-of a by Th8;
A2: a <> b by A1, Def5;
now__::_thesis:_(_a_%_is_join-irreducible_implies_a_is_completely-join-irreducible_)
assume A3: a % is join-irreducible ; ::_thesis: a is completely-join-irreducible
 for d being Element of L st d is-lower-neighbour-of a holds
d = b
proof
let d be Element of L; ::_thesis: ( d is-lower-neighbour-of a implies d = b )
A4: a % = a by LATTICE3:def_3;
A5: ( d % = d & b % = b ) by LATTICE3:def_3;
assume A6: d is-lower-neighbour-of a ; ::_thesis: d = b
then A7: a <> d by Def5;
assume  d <> b ; ::_thesis: contradiction
then  a = d "\/" b by A1, A6, Th2;
then  a % = (d %) "\/" (b %) by A4, Lm8;
hence  contradiction by A2, A3, A7, A4, A5, WAYBEL_6:def_3; ::_thesis: verum
end;
hence  a is completely-join-irreducible by A1, Th15; ::_thesis: verum
end;
hence  ( a is completely-join-irreducible iff a % is join-irreducible ) by Th18; ::_thesis: verum
end;

theorem :: LATTICE6:20
for L being finite Lattice
for a being Element of L st a <> Bottom L & a <> Top L holds
( ( a is completely-meet-irreducible implies a % is meet-irreducible ) & ( a % is meet-irreducible implies a is completely-meet-irreducible ) & ( a is completely-join-irreducible implies a % is join-irreducible ) & ( a % is join-irreducible implies a is completely-join-irreducible ) ) by Th17, Th19;

definition
let L be Lattice;
let a be Element of L;
attra is atomic  means :Def10: :: LATTICE6:def 10
a is-upper-neighbour-of Bottom L;
attra is co-atomic  means :Def11: :: LATTICE6:def 11
a is-lower-neighbour-of Top L;
end;

:: deftheorem Def10 defines atomic LATTICE6:def_10_:_
 for L being Lattice
for a being Element of L holds
( a is atomic iff a is-upper-neighbour-of Bottom L );

:: deftheorem Def11 defines co-atomic LATTICE6:def_11_:_
 for L being Lattice
for a being Element of L holds
( a is co-atomic iff a is-lower-neighbour-of Top L );

theorem :: LATTICE6:21
for L being complete Lattice
for a being Element of L st a is atomic holds
a is completely-join-irreducible
proof
let L be complete Lattice; ::_thesis: for a being Element of L st a is atomic holds
a is completely-join-irreducible
let a be Element of L; ::_thesis: ( a is atomic implies a is completely-join-irreducible )
set X =  {  x where x is Element of L : ( x [= a & x <> a )  }  ;
assume  a is atomic ; ::_thesis: a is completely-join-irreducible
then A1: a is-upper-neighbour-of Bottom L by Def10;
then A2: a <> Bottom L by Def5;
A3: for x being set st x in  {  x where x is Element of L : ( x [= a & x <> a )  }  holds
x in {(Bottom L)}
proof
let x be set ; ::_thesis: ( x in  {  x where x is Element of L : ( x [= a & x <> a )  }  implies x in {(Bottom L)} )
assume  x in  {  x where x is Element of L : ( x [= a & x <> a )  }  ; ::_thesis: x in {(Bottom L)}
then A4: ex x9 being Element of L st
( x9 = x & x9 [= a & x9 <> a ) ;
then reconsider x = x as Element of L ;
 Bottom L [= x by LATTICES:16;
then  x = Bottom L by A1, A4, Def5;
hence  x in {(Bottom L)} by TARSKI:def_1; ::_thesis: verum
end;
A5: Bottom L [= a by A1, Def5;
A6: for x being set st x in {(Bottom L)} holds
x in  {  x where x is Element of L : ( x [= a & x <> a )  }
proof
let x be set ; ::_thesis: ( x in {(Bottom L)} implies x in  {  x where x is Element of L : ( x [= a & x <> a )  }  )
assume  x in {(Bottom L)} ; ::_thesis: x in  {  x where x is Element of L : ( x [= a & x <> a )  }
then  x = Bottom L by TARSKI:def_1;
hence  x in  {  x where x is Element of L : ( x [= a & x <> a )  }  by A2, A5; ::_thesis: verum
end;
Bottom L = "\/" ({(Bottom L)},L) by LATTICE3:42
.= *' a by A3, A6, TARSKI:1 ;
hence  a is completely-join-irreducible by A2, Def9; ::_thesis: verum
end;

theorem :: LATTICE6:22
for L being complete Lattice
for a being Element of L st a is co-atomic holds
a is completely-meet-irreducible
proof
let L be complete Lattice; ::_thesis: for a being Element of L st a is co-atomic holds
a is completely-meet-irreducible
let a be Element of L; ::_thesis: ( a is co-atomic implies a is completely-meet-irreducible )
set X =  {  x where x is Element of L : ( a [= x & x <> a )  }  ;
assume  a is co-atomic ; ::_thesis: a is completely-meet-irreducible
then A1: a is-lower-neighbour-of Top L by Def11;
then A2: a <> Top L by Def5;
A3: for x being set st x in  {  x where x is Element of L : ( a [= x & x <> a )  }  holds
x in {(Top L)}
proof
let x be set ; ::_thesis: ( x in  {  x where x is Element of L : ( a [= x & x <> a )  }  implies x in {(Top L)} )
assume  x in  {  x where x is Element of L : ( a [= x & x <> a )  }  ; ::_thesis: x in {(Top L)}
then A4: ex x9 being Element of L st
( x9 = x & a [= x9 & x9 <> a ) ;
then reconsider x = x as Element of L ;
 x [= Top L by LATTICES:19;
then  x = Top L by A1, A4, Def5;
hence  x in {(Top L)} by TARSKI:def_1; ::_thesis: verum
end;
A5: a [= Top L by A1, Def5;
A6: for x being set st x in {(Top L)} holds
x in  {  x where x is Element of L : ( a [= x & x <> a )  }
proof
let x be set ; ::_thesis: ( x in {(Top L)} implies x in  {  x where x is Element of L : ( a [= x & x <> a )  }  )
assume  x in {(Top L)} ; ::_thesis: x in  {  x where x is Element of L : ( a [= x & x <> a )  }
then  x = Top L by TARSKI:def_1;
hence  x in  {  x where x is Element of L : ( a [= x & x <> a )  }  by A2, A5; ::_thesis: verum
end;
Top L = "/\" ({(Top L)},L) by LATTICE3:42
.= a *' by A3, A6, TARSKI:1 ;
hence  a is completely-meet-irreducible by A2, Def8; ::_thesis: verum
end;

definition
let L be Lattice;
attrL is atomic  means :Def12: :: LATTICE6:def 12
 for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" (X,L) );
end;

:: deftheorem Def12 defines atomic LATTICE6:def_12_:_
 for L being Lattice holds
( L is atomic iff for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" (X,L) ) );

registration
cluster non empty 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for LattStr ;
existence
 ex b1 being Lattice st
( b1 is strict & b1 is 1 -element )
proof
set X = {{}};
set XJ = the BinOp of {{}};
reconsider L = LattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}} #) as non empty LattStr ;
A1: L is trivial ;
then A2: ( ( for a, b being Element of L holds (a "/\" b) "\/" b = b ) & ( for a, b being Element of L holds a "/\" b = b "/\" a ) ) by STRUCT_0:def_10;
A3: ( ( for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c ) & ( for a, b being Element of L holds a "/\" (a "\/" b) = a ) ) by A1, STRUCT_0:def_10;
 ( ( for a, b being Element of L holds a "\/" b = b "\/" a ) & ( for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c ) ) by A1, STRUCT_0:def_10;
then  ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A2, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L = L as Lattice ;
take  L ; ::_thesis: ( L is strict & L is 1 -element )
thus  ( L is strict & L is 1 -element ) by STRUCT_0:def_19; ::_thesis: verum
end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete atomic for LattStr ;
existence
 ex b1 being Lattice st
( b1 is atomic & b1 is complete )
proof
set L = the 1 -element strict Lattice;
consider x being set  such that
A1: the carrier of the 1 -element strict Lattice = {x} by ZFMISC_1:131;
reconsider x = x as Element of the 1 -element strict Lattice by A1, TARSKI:def_1;
reconsider L = the 1 -element strict Lattice as complete Lattice ;
 for a being Element of L ex X being Subset of L st
( ( for u being Element of L st u in X holds
u is atomic ) & a = "\/" (X,L) )
proof
let a be Element of L; ::_thesis: ex X being Subset of L st
( ( for u being Element of L st u in X holds
u is atomic ) & a = "\/" (X,L) )
 for u being set st u in {} holds
u in the carrier of L ;
then A2: ( ( for u being Element of L st u in {} holds
u is atomic ) & {} is Subset of L ) by TARSKI:def_3;
 ( a = x & x = "\/" ({},L) ) by A1, TARSKI:def_1;
hence  ex X being Subset of L st
( ( for u being Element of L st u in X holds
u is atomic ) & a = "\/" (X,L) ) by A2; ::_thesis: verum
end;
then  L is atomic by Def12;
hence  ex b1 being Lattice st
( b1 is atomic & b1 is complete ) ; ::_thesis: verum
end;
end;

definition
let L be complete Lattice;
let D be Subset of L;
attrD is supremum-dense  means :Def13: :: LATTICE6:def 13
 for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L);
attrD is infimum-dense  means :Def14: :: LATTICE6:def 14
 for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L);
end;

:: deftheorem Def13 defines supremum-dense LATTICE6:def_13_:_
 for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L) );

:: deftheorem Def14 defines infimum-dense LATTICE6:def_14_:_
 for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L) );

theorem Th23: :: LATTICE6:23
for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) )
proof
let L be complete Lattice; ::_thesis: for D being Subset of L holds
( D is supremum-dense iff for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) )
let D be Subset of L; ::_thesis: ( D is supremum-dense iff for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) )
A1: now__::_thesis:_(_D_is_supremum-dense_implies_for_a_being_Element_of_L_holds_a_=_"\/"_(_{__d_where_d_is_Element_of_L_:_(_d_in_D_&_d_[=_a_)__}__,L)_)
assume A2: D is supremum-dense ; ::_thesis: for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L)
thus  for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) ::_thesis: verum
proof
let a be Element of L; ::_thesis: a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L)
set X =  {  d where d is Element of L : ( d in D & d [= a )  }  ;
consider D9 being Subset of D such that
A3: a = "\/" (D9,L) by A2, Def13;
 for x being set st x in D9 holds
x in  {  d where d is Element of L : ( d in D & d [= a )  }
proof
let x be set ; ::_thesis: ( x in D9 implies x in  {  d where d is Element of L : ( d in D & d [= a )  }  )
assume A4: x in D9 ; ::_thesis: x in  {  d where d is Element of L : ( d in D & d [= a )  }
then  x in D ;
then reconsider x = x as Element of L ;
 D9 is_less_than a by A3, LATTICE3:def_21;
then  x [= a by A4, LATTICE3:def_17;
hence  x in  {  d where d is Element of L : ( d in D & d [= a )  }  by A4; ::_thesis: verum
end;
then  D9 c=  {  d where d is Element of L : ( d in D & d [= a )  }  by TARSKI:def_3;
then A5: a [= "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) by A3, LATTICE3:45;
 for q being Element of L st q in  {  d where d is Element of L : ( d in D & d [= a )  }  holds
q [= a
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( d in D & d [= a )  }  implies q [= a )
assume  q in  {  d where d is Element of L : ( d in D & d [= a )  }  ; ::_thesis: q [= a
then  ex q9 being Element of L st
( q9 = q & q9 in D & q9 [= a ) ;
hence  q [= a ; ::_thesis: verum
end;
then   {  d where d is Element of L : ( d in D & d [= a )  }  is_less_than a by LATTICE3:def_17;
then  "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) [= a by LATTICE3:def_21;
hence  a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) by A5, LATTICES:8; ::_thesis: verum
end;
end;
now__::_thesis:_(_(_for_a_being_Element_of_L_holds_a_=_"\/"_(_{__d_where_d_is_Element_of_L_:_(_d_in_D_&_d_[=_a_)__}__,L)_)_implies_D_is_supremum-dense_)
assume A6: for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) ; ::_thesis: D is supremum-dense
 for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L)
proof
let a be Element of L; ::_thesis: ex D9 being Subset of D st a = "\/" (D9,L)
set X =  {  d where d is Element of L : ( d in D & d [= a )  }  ;
 for x being set st x in  {  d where d is Element of L : ( d in D & d [= a )  }  holds
x in D
proof
let x be set ; ::_thesis: ( x in  {  d where d is Element of L : ( d in D & d [= a )  }  implies x in D )
assume  x in  {  d where d is Element of L : ( d in D & d [= a )  }  ; ::_thesis: x in D
then  ex x9 being Element of L st
( x9 = x & x9 in D & x9 [= a ) ;
hence  x in D ; ::_thesis: verum
end;
then A7:  {  d where d is Element of L : ( d in D & d [= a )  }  is Subset of D by TARSKI:def_3;
 a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) by A6;
hence  ex D9 being Subset of D st a = "\/" (D9,L) by A7; ::_thesis: verum
end;
hence  D is supremum-dense by Def13; ::_thesis: verum
end;
hence  ( D is supremum-dense iff for a being Element of L holds a = "\/" ( {  d where d is Element of L : ( d in D & d [= a )  }  ,L) ) by A1; ::_thesis: verum
end;

theorem Th24: :: LATTICE6:24
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) )
proof
let L be complete Lattice; ::_thesis: for D being Subset of L holds
( D is infimum-dense iff for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) )
let D be Subset of L; ::_thesis: ( D is infimum-dense iff for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) )
A1: now__::_thesis:_(_D_is_infimum-dense_implies_for_a_being_Element_of_L_holds_a_=_"/\"_(_{__d_where_d_is_Element_of_L_:_(_d_in_D_&_a_[=_d_)__}__,L)_)
assume A2: D is infimum-dense ; ::_thesis: for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L)
thus  for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) ::_thesis: verum
proof
let a be Element of L; ::_thesis: a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L)
set X =  {  d where d is Element of L : ( d in D & a [= d )  }  ;
consider D9 being Subset of D such that
A3: a = "/\" (D9,L) by A2, Def14;
 for x being set st x in D9 holds
x in  {  d where d is Element of L : ( d in D & a [= d )  }
proof
let x be set ; ::_thesis: ( x in D9 implies x in  {  d where d is Element of L : ( d in D & a [= d )  }  )
assume A4: x in D9 ; ::_thesis: x in  {  d where d is Element of L : ( d in D & a [= d )  }
then  x in D ;
then reconsider x = x as Element of L ;
 a is_less_than D9 by A3, LATTICE3:34;
then  a [= x by A4, LATTICE3:def_16;
hence  x in  {  d where d is Element of L : ( d in D & a [= d )  }  by A4; ::_thesis: verum
end;
then  D9 c=  {  d where d is Element of L : ( d in D & a [= d )  }  by TARSKI:def_3;
then A5: "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) [= a by A3, LATTICE3:45;
 for q being Element of L st q in  {  d where d is Element of L : ( d in D & a [= d )  }  holds
a [= q
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( d in D & a [= d )  }  implies a [= q )
assume  q in  {  d where d is Element of L : ( d in D & a [= d )  }  ; ::_thesis: a [= q
then  ex q9 being Element of L st
( q9 = q & q9 in D & a [= q9 ) ;
hence  a [= q ; ::_thesis: verum
end;
then  a is_less_than  {  d where d is Element of L : ( d in D & a [= d )  }  by LATTICE3:def_16;
then  a [= "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) by LATTICE3:39;
hence  a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) by A5, LATTICES:8; ::_thesis: verum
end;
end;
now__::_thesis:_(_(_for_a_being_Element_of_L_holds_a_=_"/\"_(_{__d_where_d_is_Element_of_L_:_(_d_in_D_&_a_[=_d_)__}__,L)_)_implies_D_is_infimum-dense_)
assume A6: for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) ; ::_thesis: D is infimum-dense
 for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L)
proof
let a be Element of L; ::_thesis: ex D9 being Subset of D st a = "/\" (D9,L)
set X =  {  d where d is Element of L : ( d in D & a [= d )  }  ;
 for x being set st x in  {  d where d is Element of L : ( d in D & a [= d )  }  holds
x in D
proof
let x be set ; ::_thesis: ( x in  {  d where d is Element of L : ( d in D & a [= d )  }  implies x in D )
assume  x in  {  d where d is Element of L : ( d in D & a [= d )  }  ; ::_thesis: x in D
then  ex x9 being Element of L st
( x9 = x & x9 in D & a [= x9 ) ;
hence  x in D ; ::_thesis: verum
end;
then A7:  {  d where d is Element of L : ( d in D & a [= d )  }  is Subset of D by TARSKI:def_3;
 a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) by A6;
hence  ex D9 being Subset of D st a = "/\" (D9,L) by A7; ::_thesis: verum
end;
hence  D is infimum-dense by Def14; ::_thesis: verum
end;
hence  ( D is infimum-dense iff for a being Element of L holds a = "/\" ( {  d where d is Element of L : ( d in D & a [= d )  }  ,L) ) by A1; ::_thesis: verum
end;

theorem :: LATTICE6:25
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )
proof
let L be complete Lattice; ::_thesis: for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )
let D be Subset of L; ::_thesis: ( D is infimum-dense iff D % is order-generating )
A1: now__::_thesis:_(_D_%_is_order-generating_implies_D_is_infimum-dense_)
assume A2: D % is order-generating ; ::_thesis: D is infimum-dense
 for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L)
proof
let a be Element of L; ::_thesis: ex D9 being Subset of D st a = "/\" (D9,L)
consider Y being Subset of (D %) such that
A3: a % = "/\" (Y,(LattPOSet L)) by A2, WAYBEL_6:15;
A4: for x being set st x in Y holds
x in the carrier of (LattPOSet L)
proof
let x be set ; ::_thesis: ( x in Y implies x in the carrier of (LattPOSet L) )
assume  x in Y ; ::_thesis: x in the carrier of (LattPOSet L)
then  x in D % ;
hence  x in the carrier of (LattPOSet L) ; ::_thesis: verum
end;
A5: a % is_<=_than Y by A3, YELLOW_0:33;
reconsider Y = Y as Subset of (LattPOSet L) by A4, TARSKI:def_3;
A6: for b being Element of L st b is_less_than % Y holds
b [= a
proof
let b be Element of L; ::_thesis: ( b is_less_than % Y implies b [= a )
assume A7: b is_less_than % Y ; ::_thesis: b [= a
 for u being Element of (LattPOSet L) st u in Y holds
b % <= u
proof
let u be Element of (LattPOSet L); ::_thesis: ( u in Y implies b % <= u )
assume  u in Y ; ::_thesis: b % <= u
then  % u in  {  (% d) where d is Element of (LattPOSet L) : d in Y  }  ;
then A8: b [= % u by A7, LATTICE3:def_16;
(% u) % = % u by LATTICE3:def_3
.= u by LATTICE3:def_4 ;
hence  b % <= u by A8, LATTICE3:7; ::_thesis: verum
end;
then  b % is_<=_than Y by LATTICE3:def_8;
then  b % <= a % by A3, YELLOW_0:33;
hence  b [= a by LATTICE3:7; ::_thesis: verum
end;
 for x being set st x in % Y holds
x in D
proof
let x be set ; ::_thesis: ( x in % Y implies x in D )
assume  x in % Y ; ::_thesis: x in D
then consider x9 being Element of (LattPOSet L) such that
A9: x = % x9 and
A10: x9 in Y ;
 x9 in D % by A10;
then consider y being Element of L such that
A11: x9 = y % and
A12: y in D ;
x = y % by A9, A11, LATTICE3:def_4
.= y by LATTICE3:def_3 ;
hence  x in D by A12; ::_thesis: verum
end;
then A13: % Y is Subset of D by TARSKI:def_3;
 for q being Element of L st q in % Y holds
a [= q
proof
let q be Element of L; ::_thesis: ( q in % Y implies a [= q )
assume  q in % Y ; ::_thesis: a [= q
then consider q9 being Element of (LattPOSet L) such that
A14: q = % q9 and
A15: q9 in Y ;
A16: q9 = % q9 by LATTICE3:def_4
.= (% q9) % by LATTICE3:def_3 ;
 a % <= q9 by A5, A15, LATTICE3:def_8;
hence  a [= q by A14, A16, LATTICE3:7; ::_thesis: verum
end;
then  a is_less_than % Y by LATTICE3:def_16;
then  a = "/\" ((% Y),L) by A6, LATTICE3:34;
hence  ex D9 being Subset of D st a = "/\" (D9,L) by A13; ::_thesis: verum
end;
hence  D is infimum-dense by Def14; ::_thesis: verum
end;
now__::_thesis:_(_D_is_infimum-dense_implies_D_%_is_order-generating_)
assume A17: D is infimum-dense ; ::_thesis: D % is order-generating
 for a being Element of (LattPOSet L) ex Y being Subset of (D %) st a = "/\" (Y,(LattPOSet L))
proof
let a be Element of (LattPOSet L); ::_thesis: ex Y being Subset of (D %) st a = "/\" (Y,(LattPOSet L))
consider D9 being Subset of D such that
A18: % a = "/\" (D9,L) by A17, Def14;
A19: for x being set st x in D9 holds
x in the carrier of L
proof
let x be set ; ::_thesis: ( x in D9 implies x in the carrier of L )
assume  x in D9 ; ::_thesis: x in the carrier of L
then  x in D ;
hence  x in the carrier of L ; ::_thesis: verum
end;
A20: % a is_less_than D9 by A18, LATTICE3:34;
reconsider D9 = D9 as Subset of L by A19, TARSKI:def_3;
A21: for b being Element of (LattPOSet L) st D9 % is_>=_than b holds
b <= a
proof
let b be Element of (LattPOSet L); ::_thesis: ( D9 % is_>=_than b implies b <= a )
A22: b = % b by LATTICE3:def_4
.= (% b) % by LATTICE3:def_3 ;
assume A23: D9 % is_>=_than b ; ::_thesis: b <= a
 for u being Element of L st u in D9 holds
% b [= u
proof
let u be Element of L; ::_thesis: ( u in D9 implies % b [= u )
assume  u in D9 ; ::_thesis: % b [= u
then  u % in  {  (d %) where d is Element of L : d in D9  }  ;
then  b <= u % by A23, LATTICE3:def_8;
hence  % b [= u by A22, LATTICE3:7; ::_thesis: verum
end;
then  % b is_less_than D9 by LATTICE3:def_16;
then A24: % b [= % a by A18, LATTICE3:34;
a = % a by LATTICE3:def_4
.= (% a) % by LATTICE3:def_3 ;
hence  b <= a by A22, A24, LATTICE3:7; ::_thesis: verum
end;
 for x being set st x in D9 % holds
x in D %
proof
let x be set ; ::_thesis: ( x in D9 % implies x in D % )
assume  x in D9 % ; ::_thesis: x in D %
then  ex x9 being Element of L st
( x = x9 % & x9 in D9 ) ;
hence  x in D % ; ::_thesis: verum
end;
then A25: D9 % is Subset of (D %) by TARSKI:def_3;
 for u being Element of (LattPOSet L) st u in D9 % holds
a <= u
proof
let u be Element of (LattPOSet L); ::_thesis: ( u in D9 % implies a <= u )
A26: (% a) % = % a by LATTICE3:def_3
.= a by LATTICE3:def_4 ;
assume  u in D9 % ; ::_thesis: a <= u
then consider u9 being Element of L such that
A27: u = u9 % and
A28: u9 in D9 ;
 % a [= u9 by A20, A28, LATTICE3:def_16;
hence  a <= u by A27, A26, LATTICE3:7; ::_thesis: verum
end;
then  D9 % is_>=_than a by LATTICE3:def_8;
then  a = "/\" ((D9 %),(LattPOSet L)) by A21, YELLOW_0:33;
hence  ex Y being Subset of (D %) st a = "/\" (Y,(LattPOSet L)) by A25; ::_thesis: verum
end;
hence  D % is order-generating by WAYBEL_6:15; ::_thesis: verum
end;
hence  ( D is infimum-dense iff D % is order-generating ) by A1; ::_thesis: verum
end;

definition
let L be complete Lattice;
func MIRRS L ->  Subset of L equals :: LATTICE6:def 15
 {  a where a is Element of L : a is completely-meet-irreducible  }  ;
correctness
coherence
{  a where a is Element of L : a is completely-meet-irreducible  }  is Subset of L;
proof
set X =  {  a where a is Element of L : a is completely-meet-irreducible  }  ;
 for x being set st x in  {  a where a is Element of L : a is completely-meet-irreducible  }  holds
x in the carrier of L
proof
let x be set ; ::_thesis: ( x in  {  a where a is Element of L : a is completely-meet-irreducible  }  implies x in the carrier of L )
assume  x in  {  a where a is Element of L : a is completely-meet-irreducible  }  ; ::_thesis: x in the carrier of L
then  ex x9 being Element of L st
( x9 = x & x9 is completely-meet-irreducible ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
hence   {  a where a is Element of L : a is completely-meet-irreducible  }  is Subset of L by TARSKI:def_3; ::_thesis: verum
end;
func JIRRS L ->  Subset of L equals :: LATTICE6:def 16
 {  a where a is Element of L : a is completely-join-irreducible  }  ;
correctness
coherence
{  a where a is Element of L : a is completely-join-irreducible  }  is Subset of L;
proof
set X =  {  a where a is Element of L : a is completely-join-irreducible  }  ;
 for x being set st x in  {  a where a is Element of L : a is completely-join-irreducible  }  holds
x in the carrier of L
proof
let x be set ; ::_thesis: ( x in  {  a where a is Element of L : a is completely-join-irreducible  }  implies x in the carrier of L )
assume  x in  {  a where a is Element of L : a is completely-join-irreducible  }  ; ::_thesis: x in the carrier of L
then  ex x9 being Element of L st
( x9 = x & x9 is completely-join-irreducible ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
hence   {  a where a is Element of L : a is completely-join-irreducible  }  is Subset of L by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines MIRRS LATTICE6:def_15_:_
 for L being complete Lattice holds MIRRS L =  {  a where a is Element of L : a is completely-meet-irreducible  }  ;

:: deftheorem  defines JIRRS LATTICE6:def_16_:_
 for L being complete Lattice holds JIRRS L =  {  a where a is Element of L : a is completely-join-irreducible  }  ;

theorem :: LATTICE6:26
for L being complete Lattice
for D being Subset of L st D is supremum-dense holds
JIRRS L c= D
proof
let L be complete Lattice; ::_thesis: for D being Subset of L st D is supremum-dense holds
JIRRS L c= D
let D be Subset of L; ::_thesis: ( D is supremum-dense implies JIRRS L c= D )
assume A1: D is supremum-dense ; ::_thesis: JIRRS L c= D
 for x being set st x in JIRRS L holds
x in D
proof
let x be set ; ::_thesis: ( x in JIRRS L implies x in D )
assume  x in JIRRS L ; ::_thesis: x in D
then consider x9 being Element of L such that
A2: x9 = x and
A3: x9 is completely-join-irreducible ;
assume A4: not x in D ; ::_thesis: contradiction
reconsider x = x as Element of L by A2;
set D9 =  {  d where d is Element of L : ( d in D & d [= x )  }  ;
set X =  {  d where d is Element of L : ( d [= x & d <> x )  }  ;
A5: not x in  {  d where d is Element of L : ( d in D & d [= x )  }
proof
assume  x in  {  d where d is Element of L : ( d in D & d [= x )  }  ; ::_thesis: contradiction
then  ex x9 being Element of L st
( x9 = x & x9 in D & x9 [= x ) ;
hence  contradiction by A4; ::_thesis: verum
end;
 for u being set st u in  {  d where d is Element of L : ( d in D & d [= x )  }  holds
u in  {  d where d is Element of L : ( d [= x & d <> x )  }
proof
let u be set ; ::_thesis: ( u in  {  d where d is Element of L : ( d in D & d [= x )  }  implies u in  {  d where d is Element of L : ( d [= x & d <> x )  }  )
assume A6: u in  {  d where d is Element of L : ( d in D & d [= x )  }  ; ::_thesis: u in  {  d where d is Element of L : ( d [= x & d <> x )  }
then  ex u9 being Element of L st
( u9 = u & u9 in D & u9 [= x ) ;
hence  u in  {  d where d is Element of L : ( d [= x & d <> x )  }  by A5, A6; ::_thesis: verum
end;
then   {  d where d is Element of L : ( d in D & d [= x )  }  c=  {  d where d is Element of L : ( d [= x & d <> x )  }  by TARSKI:def_3;
then  "\/" ( {  d where d is Element of L : ( d in D & d [= x )  }  ,L) [= "\/" ( {  d where d is Element of L : ( d [= x & d <> x )  }  ,L) by LATTICE3:45;
then A7: x [= "\/" ( {  d where d is Element of L : ( d [= x & d <> x )  }  ,L) by A1, Th23;
 for q being Element of L st q in  {  d where d is Element of L : ( d [= x & d <> x )  }  holds
q [= x
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( d [= x & d <> x )  }  implies q [= x )
assume  q in  {  d where d is Element of L : ( d [= x & d <> x )  }  ; ::_thesis: q [= x
then  ex q9 being Element of L st
( q9 = q & q9 [= x & q9 <> x ) ;
hence  q [= x ; ::_thesis: verum
end;
then   {  d where d is Element of L : ( d [= x & d <> x )  }  is_less_than x by LATTICE3:def_17;
then A8: "\/" ( {  d where d is Element of L : ( d [= x & d <> x )  }  ,L) [= x by LATTICE3:def_21;
 *' x9 <> x9 by A3, Def9;
hence  contradiction by A2, A7, A8, LATTICES:8; ::_thesis: verum
end;
hence  JIRRS L c= D by TARSKI:def_3; ::_thesis: verum
end;

theorem :: LATTICE6:27
for L being complete Lattice
for D being Subset of L st D is infimum-dense holds
MIRRS L c= D
proof
let L be complete Lattice; ::_thesis: for D being Subset of L st D is infimum-dense holds
MIRRS L c= D
let D be Subset of L; ::_thesis: ( D is infimum-dense implies MIRRS L c= D )
assume A1: D is infimum-dense ; ::_thesis: MIRRS L c= D
 for x being set st x in MIRRS L holds
x in D
proof
let x be set ; ::_thesis: ( x in MIRRS L implies x in D )
assume  x in MIRRS L ; ::_thesis: x in D
then consider x9 being Element of L such that
A2: x9 = x and
A3: x9 is completely-meet-irreducible ;
assume A4: not x in D ; ::_thesis: contradiction
reconsider x = x as Element of L by A2;
set D9 =  {  d where d is Element of L : ( d in D & x [= d )  }  ;
set X =  {  d where d is Element of L : ( x [= d & d <> x )  }  ;
A5: not x in  {  d where d is Element of L : ( d in D & x [= d )  }
proof
assume  x in  {  d where d is Element of L : ( d in D & x [= d )  }  ; ::_thesis: contradiction
then  ex x9 being Element of L st
( x9 = x & x9 in D & x [= x9 ) ;
hence  contradiction by A4; ::_thesis: verum
end;
 for u being set st u in  {  d where d is Element of L : ( d in D & x [= d )  }  holds
u in  {  d where d is Element of L : ( x [= d & d <> x )  }
proof
let u be set ; ::_thesis: ( u in  {  d where d is Element of L : ( d in D & x [= d )  }  implies u in  {  d where d is Element of L : ( x [= d & d <> x )  }  )
assume A6: u in  {  d where d is Element of L : ( d in D & x [= d )  }  ; ::_thesis: u in  {  d where d is Element of L : ( x [= d & d <> x )  }
then  ex u9 being Element of L st
( u9 = u & u9 in D & x [= u9 ) ;
hence  u in  {  d where d is Element of L : ( x [= d & d <> x )  }  by A5, A6; ::_thesis: verum
end;
then   {  d where d is Element of L : ( d in D & x [= d )  }  c=  {  d where d is Element of L : ( x [= d & d <> x )  }  by TARSKI:def_3;
then  "/\" ( {  d where d is Element of L : ( x [= d & d <> x )  }  ,L) [= "/\" ( {  d where d is Element of L : ( d in D & x [= d )  }  ,L) by LATTICE3:45;
then A7: "/\" ( {  d where d is Element of L : ( x [= d & d <> x )  }  ,L) [= x by A1, Th24;
 for q being Element of L st q in  {  d where d is Element of L : ( x [= d & d <> x )  }  holds
x [= q
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( x [= d & d <> x )  }  implies x [= q )
assume  q in  {  d where d is Element of L : ( x [= d & d <> x )  }  ; ::_thesis: x [= q
then  ex q9 being Element of L st
( q9 = q & x [= q9 & q9 <> x ) ;
hence  x [= q ; ::_thesis: verum
end;
then  x is_less_than  {  d where d is Element of L : ( x [= d & d <> x )  }  by LATTICE3:def_16;
then A8: x [= "/\" ( {  d where d is Element of L : ( x [= d & d <> x )  }  ,L) by LATTICE3:39;
 x9 *' <> x9 by A3, Def8;
hence  contradiction by A2, A7, A8, LATTICES:8; ::_thesis: verum
end;
hence  MIRRS L c= D by TARSKI:def_3; ::_thesis: verum
end;

Lm9:  for L being complete co-noetherian Lattice holds MIRRS L is infimum-dense
proof
let L be complete co-noetherian Lattice; ::_thesis: MIRRS L is infimum-dense
defpred S1[ Element of ((LattPOSet L) ~)] means  ex D9 being Subset of (MIRRS L) st $1 = ("/\" (D9,L)) % ;
A1: for x being Element of ((LattPOSet L) ~) st ( for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ) holds
S1[x]
proof
let x be Element of ((LattPOSet L) ~); ::_thesis: ( ( for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ) implies S1[x] )
set X =  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  ;
A2: for u being Element of L st u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  holds
( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) )
proof
let u be Element of L; ::_thesis: ( u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  implies ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) ) )
A3: ((% (~ x)) %) ~ = (% (~ x)) % by LATTICE3:def_6
.= % (~ x) by LATTICE3:def_3
.= ~ x by LATTICE3:def_4
.= x by LATTICE3:def_7 ;
assume  u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  ; ::_thesis: ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) )
then A4: ex u9 being Element of L st
( u9 = u & % (~ x) [= u9 & % (~ x) <> u9 ) ;
then  (% (~ x)) % <= u % by LATTICE3:7;
then A5: (u %) ~ <= x by A3, LATTICE3:9;
A6: (u %) ~ = u % by LATTICE3:def_6
.= u by LATTICE3:def_3 ;
% (~ x) = ~ x by LATTICE3:def_4
.= x by LATTICE3:def_7 ;
hence  ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) ) by A4, A5, A6, ORDERS_2:def_5; ::_thesis: verum
end;
assume A7: for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ; ::_thesis: S1[x]
A8: for u being Element of L st u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  holds
S1[(u %) ~ ]
proof
let u be Element of L; ::_thesis: ( u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  implies S1[(u %) ~ ] )
assume  u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  ; ::_thesis: S1[(u %) ~ ]
then  ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) ) by A2;
hence  S1[(u %) ~ ] by A7; ::_thesis: verum
end;
percases ( % (~ x) is completely-meet-irreducible or not % (~ x) is completely-meet-irreducible ) ;
suppose % (~ x) is completely-meet-irreducible ; ::_thesis: S1[x]
then  % (~ x) in  {  a where a is Element of L : a is completely-meet-irreducible  }  ;
then  for y being set st y in {(% (~ x))} holds
y in MIRRS L by TARSKI:def_1;
then A9: {(% (~ x))} is Subset of (MIRRS L) by TARSKI:def_3;
("/\" ({(% (~ x))},L)) % = "/\" ({(% (~ x))},L) by LATTICE3:def_3
.= % (~ x) by LATTICE3:42
.= ~ x by LATTICE3:def_4
.= x by LATTICE3:def_7 ;
hence  S1[x] by A9; ::_thesis: verum
end;
supposeA10: not % (~ x) is completely-meet-irreducible ; ::_thesis: S1[x]
set G =  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ;
set D9 = union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ;
A11: (% (~ x)) *' = % (~ x) by A10, Def8;
A12: for r being Element of L st r is_less_than union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  holds
r [= % (~ x)
proof
let r be Element of L; ::_thesis: ( r is_less_than union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  implies r [= % (~ x) )
assume A13: r is_less_than union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ; ::_thesis: r [= % (~ x)
 for q being Element of L st q in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  holds
r [= q
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  implies r [= q )
assume A14: q in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  ; ::_thesis: r [= q
then consider D being Subset of (MIRRS L) such that
A15: (q %) ~ = ("/\" (D,L)) % by A8;
A16: q % = q by LATTICE3:def_3;
 for v being set st v in D holds
v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }
proof
let v be set ; ::_thesis: ( v in D implies v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  )
(q %) ~ = q % by LATTICE3:def_6
.= % (q %) by LATTICE3:def_4 ;
then A17: % (q %) = "/\" (D,L) by A15, LATTICE3:def_3;
 % (q %) in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  by A14, A16, LATTICE3:def_4;
then A18: D in  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  by A17;
assume  v in D ; ::_thesis: v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }
hence  v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  by A18, TARSKI:def_4; ::_thesis: verum
end;
then  D c= union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  by TARSKI:def_3;
then  for p being Element of L st p in D holds
r [= p by A13, LATTICE3:def_16;
then A19: r is_less_than D by LATTICE3:def_16;
q = (q %) ~ by A16, LATTICE3:def_6
.= "/\" (D,L) by A15, LATTICE3:def_3 ;
hence  r [= q by A19, LATTICE3:34; ::_thesis: verum
end;
then  r is_less_than  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  by LATTICE3:def_16;
hence  r [= % (~ x) by A11, LATTICE3:34; ::_thesis: verum
end;
 for v being set st v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  holds
v in MIRRS L
proof
let v be set ; ::_thesis: ( v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  implies v in MIRRS L )
assume  v in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ; ::_thesis: v in MIRRS L
then consider v9 being set  such that
A20: v in v9 and
A21: v9 in  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  by TARSKI:def_4;
 ex H being Subset of (MIRRS L) st
( H = v9 & ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) ) ) by A21;
hence  v in MIRRS L by A20; ::_thesis: verum
end;
then A22: union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  is Subset of (MIRRS L) by TARSKI:def_3;
A23: % (~ x) = ~ x by LATTICE3:def_4
.= x by LATTICE3:def_7 ;
A24: ("/\" ((union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ),L)) % = "/\" ((union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ),L) by LATTICE3:def_3;
 for q being Element of L st q in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  holds
% (~ x) [= q
proof
let q be Element of L; ::_thesis: ( q in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  implies % (~ x) [= q )
assume  q in union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ; ::_thesis: % (~ x) [= q
then consider h being set  such that
A25: q in h and
A26: h in  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  by TARSKI:def_4;
 ex h9 being Subset of (MIRRS L) st
( h9 = h & ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (h9,L) ) ) by A26;
then consider u being Element of (LattPOSet L) such that
A27: % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  and
A28: % u = "/\" (h,L) ;
 % u is_less_than h by A28, LATTICE3:34;
then A29: % u [= q by A25, LATTICE3:def_16;
 % (~ x) is_less_than  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  by A11, LATTICE3:34;
then  % (~ x) [= % u by A27, LATTICE3:def_16;
hence  % (~ x) [= q by A29, LATTICES:7; ::_thesis: verum
end;
then  % (~ x) is_less_than union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  by LATTICE3:def_16;
then  % (~ x) = "/\" ((union  {  H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) )  }  & % u = "/\" (H,L) )  }  ),L) by A12, LATTICE3:34;
hence  S1[x] by A22, A23, A24; ::_thesis: verum
end;
end;
end;
A30: (LattPOSet L) ~ is well_founded by Def4;
A31: for x being Element of ((LattPOSet L) ~) holds S1[x] from WELLFND1:sch_3(A1, A30);
 for a being Element of L ex D9 being Subset of (MIRRS L) st a = "/\" (D9,L)
proof
let a be Element of L; ::_thesis: ex D9 being Subset of (MIRRS L) st a = "/\" (D9,L)
 (LattPOSet L) ~ = RelStr(# the carrier of (LattPOSet L),( the InternalRel of (LattPOSet L) ~) #) by LATTICE3:def_5;
then reconsider a9 = a % as Element of ((LattPOSet L) ~) ;
 ( ex D9 being Subset of (MIRRS L) st a9 = ("/\" (D9,L)) % & a % = a ) by A31, LATTICE3:def_3;
hence  ex D9 being Subset of (MIRRS L) st a = "/\" (D9,L) by LATTICE3:def_3; ::_thesis: verum
end;
hence  MIRRS L is infimum-dense by Def14; ::_thesis: verum
end;

registration
let L be complete co-noetherian Lattice;
cluster MIRRS L ->  infimum-dense ;
coherence
 MIRRS L is infimum-dense by Lm9;
end;

Lm10:  for L being complete noetherian Lattice holds JIRRS L is supremum-dense
proof
let L be complete noetherian Lattice; ::_thesis: JIRRS L is supremum-dense
defpred S1[ Element of (LattPOSet L)] means  ex D9 being Subset of (JIRRS L) st % $1 = "\/" (D9,L);
A1: for x being Element of (LattPOSet L) st ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ) holds
S1[x]
proof
let x be Element of (LattPOSet L); ::_thesis: ( ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ) implies S1[x] )
set X =  {  d where d is Element of L : ( d [= % x & d <> % x )  }  ;
A2: for u being Element of L st u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  holds
( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) )
proof
let u be Element of L; ::_thesis: ( u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  implies ( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) ) )
assume  u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  ; ::_thesis: ( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) )
then A3: ex u9 being Element of L st
( u9 = u & u9 [= % x & % x <> u9 ) ;
A4: % x = x by LATTICE3:def_4;
then  (% x) % = x by LATTICE3:def_3;
then  u % <= x by A3, LATTICE3:7;
hence  ( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) ) by A3, A4, LATTICE3:def_3, ORDERS_2:def_5; ::_thesis: verum
end;
assume A5: for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ; ::_thesis: S1[x]
A6: for u being Element of L st u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  holds
S1[u % ]
proof
let u be Element of L; ::_thesis: ( u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  implies S1[u % ] )
assume  u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  ; ::_thesis: S1[u % ]
then  ( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) ) by A2;
hence  S1[u % ] by A5; ::_thesis: verum
end;
percases ( % x is completely-join-irreducible or not % x is completely-join-irreducible ) ;
suppose % x is completely-join-irreducible ; ::_thesis: S1[x]
then  % x in  {  a where a is Element of L : a is completely-join-irreducible  }  ;
then  for y being set st y in {(% x)} holds
y in JIRRS L by TARSKI:def_1;
then A7: {(% x)} is Subset of (JIRRS L) by TARSKI:def_3;
 "\/" ({(% x)},L) = % x by LATTICE3:42;
hence  S1[x] by A7; ::_thesis: verum
end;
supposeA8: not % x is completely-join-irreducible ; ::_thesis: S1[x]
set G =  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  ;
set D9 = union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  ;
A9: *' (% x) = % x by A8, Def9;
A10: for r being Element of L st union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  is_less_than r holds
% x [= r
proof
let r be Element of L; ::_thesis: ( union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  is_less_than r implies % x [= r )
assume A11: union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  is_less_than r ; ::_thesis: % x [= r
 for q being Element of L st q in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  holds
q [= r
proof
let q be Element of L; ::_thesis: ( q in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  implies q [= r )
assume A12: q in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  ; ::_thesis: q [= r
then consider D being Subset of (JIRRS L) such that
A13: % (q %) = "\/" (D,L) by A6;
 q % = q by LATTICE3:def_3;
then A14: q = "\/" (D,L) by A13, LATTICE3:def_4;
 for v being set st v in D holds
v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }
proof
let v be set ; ::_thesis: ( v in D implies v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  )
assume A15: v in D ; ::_thesis: v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }
 D in  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  by A12, A13, A14;
hence  v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  by A15, TARSKI:def_4; ::_thesis: verum
end;
then  D c= union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  by TARSKI:def_3;
then  for p being Element of L st p in D holds
p [= r by A11, LATTICE3:def_17;
then  D is_less_than r by LATTICE3:def_17;
hence  q [= r by A14, LATTICE3:def_21; ::_thesis: verum
end;
then   {  d where d is Element of L : ( d [= % x & d <> % x )  }  is_less_than r by LATTICE3:def_17;
hence  % x [= r by A9, LATTICE3:def_21; ::_thesis: verum
end;
 for v being set st v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  holds
v in JIRRS L
proof
let v be set ; ::_thesis: ( v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  implies v in JIRRS L )
assume  v in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  ; ::_thesis: v in JIRRS L
then consider v9 being set  such that
A16: v in v9 and
A17: v9 in  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  by TARSKI:def_4;
 ex H being Subset of (JIRRS L) st
( H = v9 & ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) ) ) by A17;
hence  v in JIRRS L by A16; ::_thesis: verum
end;
then A18: union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  is Subset of (JIRRS L) by TARSKI:def_3;
 for q being Element of L st q in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  holds
q [= % x
proof
let q be Element of L; ::_thesis: ( q in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  implies q [= % x )
assume  q in union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  ; ::_thesis: q [= % x
then consider h being set  such that
A19: q in h and
A20: h in  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  by TARSKI:def_4;
 ex h9 being Subset of (JIRRS L) st
( h9 = h & ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (h9,L) ) ) by A20;
then consider u being Element of (LattPOSet L) such that
A21: % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  and
A22: % u = "\/" (h,L) ;
 h is_less_than % u by A22, LATTICE3:def_21;
then A23: q [= % u by A19, LATTICE3:def_17;
  {  d where d is Element of L : ( d [= % x & d <> % x )  }  is_less_than % x by A9, LATTICE3:def_21;
then  % u [= % x by A21, LATTICE3:def_17;
hence  q [= % x by A23, LATTICES:7; ::_thesis: verum
end;
then  union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  is_less_than % x by LATTICE3:def_17;
then  % x = "\/" ((union  {  H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in  {  d where d is Element of L : ( d [= % x & d <> % x )  }  & % u = "\/" (H,L) )  }  ),L) by A10, LATTICE3:def_21;
hence  S1[x] by A18; ::_thesis: verum
end;
end;
end;
A24: LattPOSet L is well_founded by Def3;
A25: for x being Element of (LattPOSet L) holds S1[x] from WELLFND1:sch_3(A1, A24);
 for a being Element of L ex D9 being Subset of (JIRRS L) st a = "\/" (D9,L)
proof
let a be Element of L; ::_thesis: ex D9 being Subset of (JIRRS L) st a = "\/" (D9,L)
% (a %) = a % by LATTICE3:def_4
.= a by LATTICE3:def_3 ;
hence  ex D9 being Subset of (JIRRS L) st a = "\/" (D9,L) by A25; ::_thesis: verum
end;
hence  JIRRS L is supremum-dense by Def13; ::_thesis: verum
end;

registration
let L be complete noetherian Lattice;
cluster JIRRS L ->  supremum-dense ;
coherence
 JIRRS L is supremum-dense by Lm10;
end;