\import Algebra.Pointed
\import Set

\class SubPointed \extends SubSet {
  \override S : Pointed
  | contains_ide : contains 

  \func struct : Pointed \cowith
    | BaseSet => SubSet.struct
    | ide => (, contains_ide)
} \where {
  \func max {A : Pointed} : SubPointed \cowith
    | SubSet => DecSubSet.max {A}
    | contains_ide => ()
}

\class DecSubPointed \extends SubPointed, DecSubSet

\class SubAddPointed \extends SubSet {
  \override S : AddPointed
  | contains_zro : contains 

  \func struct : AddPointed \cowith
    | BaseSet => SubSet.struct
    | zro => (, contains_zro)
} \where {
  \func max {A : AddPointed} : SubAddPointed \cowith
    | SubSet => DecSubSet.max {A}
    | contains_zro => ()
}