:: 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 ) ;
end;

registration
cluster non empty finite Lattice-like -> non empty Lattice-like complete for ( ( ) ( ) LattStr ) ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let D be ( ( ) ( ) Subset of ) ;
func D % -> ( ( ) ( ) Subset of ) equals :: LATTICE6:def 1
 { (d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) %) : ( ( ) ( ) Element of the carrier of (LattPOSet L : ( ( non empty ) ( non empty ) set ) ) : ( ( strict reflexive transitive antisymmetric ) ( strict V157() reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) where d is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) set ) } ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let D be ( ( ) ( ) Subset of ) ;
func % D -> ( ( ) ( ) Subset of ) equals :: LATTICE6:def 2
 { (% d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) where d is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) set ) } ;
end;

registration
let L be ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ;
cluster LattPOSet L : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) LattStr ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) -> strict reflexive transitive antisymmetric well_founded ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
attr L is noetherian means :: LATTICE6:def 3
 LattPOSet L : ( ( non empty ) ( non empty ) set ) : ( ( strict reflexive transitive antisymmetric ) ( strict V157() reflexive transitive antisymmetric ) RelStr ) is well_founded ;
attr L is co-noetherian means :: LATTICE6:def 4
(LattPOSet L : ( ( non empty ) ( non empty ) set ) ) : ( ( strict reflexive transitive antisymmetric ) ( strict V157() reflexive transitive antisymmetric ) RelStr ) ~ : ( ( strict ) ( strict V157() reflexive transitive antisymmetric ) RelStr ) is well_founded ;
end;

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 ) ;
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 ) ;
end;

theorem :: LATTICE6:1
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) holds
( L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is noetherian iff L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) .: : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) is co-noetherian ) ;

registration
cluster non empty finite Lattice-like -> non empty Lattice-like noetherian for ( ( ) ( ) LattStr ) ;
cluster non empty finite Lattice-like -> non empty Lattice-like co-noetherian for ( ( ) ( ) LattStr ) ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred a is-upper-neighbour-of b means :: LATTICE6:def 5
( a : ( ( non empty ) ( non empty ) set ) <> b : ( ( Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & b : ( ( Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) [= a : ( ( non empty ) ( non empty ) set ) & ( for c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st b : ( ( Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) [= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= a : ( ( non empty ) ( non empty ) set ) & not c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( non empty ) ( non empty ) set ) holds
c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like Function-like V20([:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) );
end;

notation
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;
end;

theorem :: LATTICE6:2
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: LATTICE6:3
for L being ( ( non empty Lattice-like noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like noetherian ) Lattice)
for a, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE6:4
for L being ( ( non empty Lattice-like co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like co-noetherian ) Lattice)
for a, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE6:5
for L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of Top L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE6:6
for L being ( ( non empty Lattice-like upper-bounded noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Top L : ( ( non empty Lattice-like upper-bounded noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded noetherian ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded noetherian ) Lattice) : ( ( ) ( non empty ) set ) ) iff for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE6:7
for L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of Bottom L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE6:8
for L being ( ( non empty Lattice-like lower-bounded co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded co-noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Bottom L : ( ( non empty Lattice-like lower-bounded co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded co-noetherian ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded co-noetherian ) Lattice) : ( ( ) ( non empty ) set ) ) iff for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

definition
let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func a *' -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: LATTICE6:def 6
 "/\" ( { d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where d is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( a : ( ( non empty ) ( non empty ) set ) [= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> a : ( ( non empty ) ( non empty ) set ) ) } ,L : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
func *' a -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: LATTICE6:def 7
 "\/" ( { d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where d is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= a : ( ( non empty ) ( non empty ) set ) & d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> a : ( ( non empty ) ( non empty ) set ) ) } ,L : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr a is completely-meet-irreducible means :: LATTICE6:def 8
a : ( ( non empty ) ( non empty ) set ) *' : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( non empty ) ( non empty ) set ) ;
attr a is completely-join-irreducible means :: LATTICE6:def 9
 *' a : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( non empty ) ( non empty ) set ) ;
end;

theorem :: LATTICE6:9
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *' : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & *' a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE6:10
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) holds
( (Top L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) *' : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Top L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) & (Top L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) is meet-irreducible ) ;

theorem :: LATTICE6:11
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) holds
( *' (Bottom L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Bottom L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) & (Bottom L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) is join-irreducible ) ;

theorem :: LATTICE6:12
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-meet-irreducible holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *' : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *' : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: LATTICE6:13
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-join-irreducible holds
( *' a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = *' a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: LATTICE6:14
for L being ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-meet-irreducible iff ex b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-upper-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: LATTICE6:15
for L being ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-join-irreducible iff ex b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is-lower-neighbour-of a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: LATTICE6:16
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-meet-irreducible holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) is meet-irreducible ;

theorem :: LATTICE6:17
for L being ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> Top L : ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) Lattice) : ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-meet-irreducible iff a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) is meet-irreducible ) ;

theorem :: LATTICE6:18
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-join-irreducible holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) is join-irreducible ;

theorem :: LATTICE6:19
for L being ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> Bottom L : ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) Lattice) : ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-join-irreducible iff a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) is join-irreducible ) ;

theorem :: LATTICE6:20
for L being ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) <> Bottom L : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) : ( ( ) ( non empty finite ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) <> Top L : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) : ( ( ) ( non empty finite ) set ) ) holds
( ( a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) is completely-meet-irreducible implies a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded ) RelStr ) : ( ( ) ( non empty ) set ) ) is meet-irreducible ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded ) RelStr ) : ( ( ) ( non empty ) set ) ) is meet-irreducible implies a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) is completely-meet-irreducible ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) is completely-join-irreducible implies a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded ) RelStr ) : ( ( ) ( non empty ) set ) ) is join-irreducible ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) % : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty finite Lattice-like ) ( non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian co-noetherian ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded ) RelStr ) : ( ( ) ( non empty ) set ) ) is join-irreducible implies a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) is completely-join-irreducible ) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr a is atomic means :: LATTICE6:def 10
a : ( ( non empty ) ( non empty ) set ) is-upper-neighbour-of Bottom L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
attr a is co-atomic means :: LATTICE6:def 11
a : ( ( non empty ) ( non empty ) set ) is-lower-neighbour-of Top L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: LATTICE6:21
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atomic holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-join-irreducible ;

theorem :: LATTICE6:22
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-atomic holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-meet-irreducible ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
attr L is atomic means :: LATTICE6:def 12
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex X being ( ( ) ( ) Subset of ) st
( ( for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atomic ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "\/" (X : ( ( ) ( ) Subset of ) ,L : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) );
end;

registration
cluster non empty 1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() non finite V40() V41() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for ( ( ) ( ) LattStr ) ;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete atomic for ( ( ) ( ) LattStr ) ;
end;

definition
let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ;
let D be ( ( ) ( ) Subset of ) ;
attr D is supremum-dense means :: LATTICE6:def 13
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex D9 being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "\/" (D9 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,L : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
attr D is infimum-dense means :: LATTICE6:def 14
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex D9 being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "/\" (D9 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,L : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: LATTICE6:23
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for D being ( ( ) ( ) Subset of ) holds
( D : ( ( ) ( ) Subset of ) is supremum-dense iff for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "\/" ( { d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where d is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( ) ( ) Subset of ) & d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) } ,L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE6:24
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for D being ( ( ) ( ) Subset of ) holds
( D : ( ( ) ( ) Subset of ) is infimum-dense iff for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "/\" ( { d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where d is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) } ,L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE6:25
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for D being ( ( ) ( ) Subset of ) holds
( D : ( ( ) ( ) Subset of ) is infimum-dense iff D : ( ( ) ( ) Subset of ) % : ( ( ) ( ) Subset of ) is order-generating ) ;

definition
let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) ;
func MIRRS L -> ( ( ) ( ) Subset of ) equals :: LATTICE6:def 15
 { a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where a is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-meet-irreducible } ;
func JIRRS L -> ( ( ) ( ) Subset of ) equals :: LATTICE6:def 16
 { a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where a is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-join-irreducible } ;
end;

theorem :: LATTICE6:26
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for D being ( ( ) ( ) Subset of ) st D : ( ( ) ( ) Subset of ) is supremum-dense holds
JIRRS L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( ) Subset of ) c= D : ( ( ) ( ) Subset of ) ;

theorem :: LATTICE6:27
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice)
for D being ( ( ) ( ) Subset of ) st D : ( ( ) ( ) Subset of ) is infimum-dense holds
MIRRS L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete ) Lattice) : ( ( ) ( ) Subset of ) c= D : ( ( ) ( ) Subset of ) ;

registration
let L be ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) Lattice) ;
cluster MIRRS L : ( ( non empty Lattice-like complete co-noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete co-noetherian ) LattStr ) : ( ( ) ( ) Subset of ) -> infimum-dense ;
end;

registration
let L be ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) Lattice) ;
cluster JIRRS L : ( ( non empty Lattice-like complete noetherian ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete noetherian ) LattStr ) : ( ( ) ( ) Subset of ) -> supremum-dense ;
end;