for L being non empty LattStr
for S being non empty ClosedSubset of L holds
( ( L is meet-associative implies latt (L,S) is meet-associative ) & ( L is meet-absorbing implies latt (L,S) is meet-absorbing ) & ( L is meet-commutative implies latt (L,S) is meet-commutative ) & ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )