:: MSUALG_7 semantic presentation

begin

theorem :: MSUALG_7:1
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) holds id M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedFunction of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) is ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: MSUALG_7:2
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) holds [|M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) is ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let M be ( ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster EqRelLatt M : ( ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -> non empty strict Lattice-like bounded ;
end;

theorem :: MSUALG_7:3
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) holds Bottom (EqRelLatt M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( ) Element of the carrier of (EqRelLatt b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( non empty ) set ) ) = id M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedFunction of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: MSUALG_7:4
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) holds Top (EqRelLatt M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( ) Element of the carrier of (EqRelLatt b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( non empty ) set ) ) = [|M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ;

theorem :: MSUALG_7:5
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of ) holds X : ( ( ) ( ) Subset of ) is ( ( ) ( ) SubsetFamily of ) ;

theorem :: MSUALG_7:6
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A, B being ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = A : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = B : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff A : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) c= B : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ;

theorem :: MSUALG_7:7
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of )
for X1 being ( ( ) ( ) SubsetFamily of ) st X1 : ( ( ) ( ) SubsetFamily of ) = X : ( ( ) ( ) Subset of ) holds
for a, b being ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) st a : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) = meet |:X1 : ( ( ) ( ) SubsetFamily of ) :| : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of K200(b1 : ( ( non empty ) ( non empty ) set ) ,[|b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of [|b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) & b : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) in X : ( ( ) ( ) Subset of ) holds
a : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) c= b : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: MSUALG_7:8
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of )
for X1 being ( ( ) ( ) SubsetFamily of ) st X1 : ( ( ) ( ) SubsetFamily of ) = X : ( ( ) ( ) Subset of ) & not X : ( ( ) ( ) Subset of ) is empty holds
meet |:X1 : ( ( ) ( ) SubsetFamily of ) :| : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of K200(b1 : ( ( non empty ) ( non empty ) set ) ,[|b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of [|b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) is ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

definition
let L be ( ( non empty ) ( non empty ) LattStr ) ;
redefine attr L is complete means :: MSUALG_7:def 1
 for X being ( ( ) ( ) Subset of ) ex a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( X : ( ( ) ( ) Subset of ) is_less_than a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ) is_less_than b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: MSUALG_7:9
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) holds EqRelLatt M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) LattStr ) is complete ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let M be ( ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster EqRelLatt M : ( ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(I : ( ( non empty ) ( non empty ) set ) ) Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) LattStr ) -> non empty strict Lattice-like complete ;
end;

theorem :: MSUALG_7:10
for I being ( ( non empty ) ( non empty ) set )
for M being ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of )
for X1 being ( ( ) ( ) SubsetFamily of ) st X1 : ( ( ) ( ) SubsetFamily of ) = X : ( ( ) ( ) Subset of ) & not X : ( ( ) ( ) Subset of ) is empty holds
for a, b being ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) st a : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) = meet |:X1 : ( ( ) ( ) SubsetFamily of ) :| : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of K200(b1 : ( ( non empty ) ( non empty ) set ) ,[|b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of [|b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) |] : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) & b : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) = "/\" (X : ( ( ) ( ) Subset of ) ,(EqRelLatt M : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (EqRelLatt b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) : ( ( ) ( non empty ) set ) ) holds
a : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) = b : ( ( MSEquivalence_Relation-like ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) MSEquivalence_Relation-like ) Equivalence_Relation of b2 : ( ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4(b1 : ( ( non empty ) ( non empty ) set ) ) Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

begin

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 IT be ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
attr IT is /\-inheriting means :: MSUALG_7:def 2
 for X being ( ( ) ( ) Subset of ) holds "/\" (X : ( ( ) ( ) Subset of ) ,L : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in the carrier of IT : ( ( V1() V4(L : ( ( ) ( ) 1-sorted ) ) Function-like V14(L : ( ( ) ( ) 1-sorted ) ) ) ( V1() V4(L : ( ( ) ( ) 1-sorted ) ) Function-like V14(L : ( ( ) ( ) 1-sorted ) ) ) set ) : ( ( ) ( ) set ) ;
attr IT is \/-inheriting means :: MSUALG_7:def 3
 for X being ( ( ) ( ) Subset of ) holds "\/" (X : ( ( ) ( ) Subset of ) ,L : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in the carrier of IT : ( ( V1() V4(L : ( ( ) ( ) 1-sorted ) ) Function-like V14(L : ( ( ) ( ) 1-sorted ) ) ) ( V1() V4(L : ( ( ) ( ) 1-sorted ) ) Function-like V14(L : ( ( ) ( ) 1-sorted ) ) ) set ) : ( ( ) ( ) set ) ;
end;

theorem :: MSUALG_7:11
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 L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a9, b9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) 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 ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice 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 ) ) & a : ( ( ) ( ) 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 ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice 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 :: MSUALG_7:12
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 L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) )
for X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_less_than X : ( ( ) ( ) Subset of ) iff a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_less_than X : ( ( ) ( ) Subset of ) ) ;

theorem :: MSUALG_7:13
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 L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) )
for X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Subset of ) is_less_than a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff X : ( ( ) ( ) Subset of ) is_less_than a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: MSUALG_7:14
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice)
for L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is /\-inheriting holds
L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is complete ;

theorem :: MSUALG_7:15
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice)
for L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is \/-inheriting holds
L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is complete ;

registration
let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete for ( ( ) ( ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ;
end;

registration
let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ;
cluster /\-inheriting -> complete for ( ( ) ( ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ;
cluster \/-inheriting -> complete for ( ( ) ( ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ;
end;

theorem :: MSUALG_7: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 complete ) Lattice)
for L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is /\-inheriting holds
for A9 being ( ( ) ( ) Subset of ) holds "/\" (A9 : ( ( ) ( ) Subset of ) ,L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like 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 complete ) Lattice) : ( ( ) ( non empty ) set ) ) = "/\" (A9 : ( ( ) ( ) Subset of ) ,L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MSUALG_7:17
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice)
for L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is \/-inheriting holds
for A9 being ( ( ) ( ) Subset of ) holds "\/" (A9 : ( ( ) ( ) Subset of ) ,L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like 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 complete ) Lattice) : ( ( ) ( non empty ) set ) ) = "\/" (A9 : ( ( ) ( ) Subset of ) ,L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MSUALG_7: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 complete ) Lattice)
for L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is /\-inheriting holds
for A being ( ( ) ( ) Subset of )
for A9 being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = A9 : ( ( ) ( ) Subset of ) holds
"/\" A : ( ( ) ( ) Subset of ) : ( ( ) ( ) 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 complete ) Lattice) : ( ( ) ( non empty ) set ) ) = "/\" A9 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MSUALG_7:19
for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice)
for L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is \/-inheriting holds
for A being ( ( ) ( ) Subset of )
for A9 being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = A9 : ( ( ) ( ) Subset of ) holds
"\/" A : ( ( ) ( ) Subset of ) : ( ( ) ( ) 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 complete ) Lattice) : ( ( ) ( non empty ) set ) ) = "\/" A9 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) : ( ( ) ( non empty ) set ) ) ;

begin

definition
let r1, r2 be ( ( ) ( V31() V32() ext-real ) Real) ;
assume r1 : ( ( ) ( V31() V32() ext-real ) Real) <= r2 : ( ( ) ( V31() V32() ext-real ) Real) ;
func RealSubLatt (r1,r2) -> ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) means :: MSUALG_7:def 4
( the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = [.r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ,r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) .] : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) & the L_join of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) Function-like V18([: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = maxreal : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ) ) ( V1() V4([:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) ) V5( REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ) Function-like V18([:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || [.r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ,r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) .] : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V1() Function-like ) set ) & the L_meet of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) Function-like V18([: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of bool (Bool r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = minreal : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ) ) ( V1() V4([:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) ) V5( REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ) Function-like V18([:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || [.r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ,r2 : ( ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) ( V1() V4(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) Function-like V14(r1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) ) ) set ) .] : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V1() Function-like ) set ) );
end;

theorem :: MSUALG_7:20
for r1, r2 being ( ( ) ( V31() V32() ext-real ) Real) st r1 : ( ( ) ( V31() V32() ext-real ) Real) <= r2 : ( ( ) ( V31() V32() ext-real ) Real) holds
RealSubLatt (r1 : ( ( ) ( V31() V32() ext-real ) Real) ,r2 : ( ( ) ( V31() V32() ext-real ) Real) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is complete ;

theorem :: MSUALG_7:21
ex L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of RealSubLatt (0 : ( ( ) ( empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st
( L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of RealSubLatt (0 : ( ( ) ( empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is \/-inheriting & not L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of RealSubLatt (0 : ( ( ) ( empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is /\-inheriting ) ;

theorem :: MSUALG_7:22
ex L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ex L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st
( L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is \/-inheriting & not L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is /\-inheriting ) ;

theorem :: MSUALG_7:23
ex L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of RealSubLatt (0 : ( ( ) ( empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st
( L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of RealSubLatt (0 : ( ( ) ( empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is /\-inheriting & not L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of RealSubLatt (0 : ( ( ) ( empty natural V31() V32() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V31() V32() ext-real positive non negative V36() V37() V38() V39() V40() V41() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V59() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is \/-inheriting ) ;

theorem :: MSUALG_7:24
ex L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ex L9 being ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) st
( L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is /\-inheriting & not L9 : ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of b1 : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) is \/-inheriting ) ;