The set S is a subset of T if all the elements in S are in T. If S equals T, S is still a subset of T meaning (-> (=_ S T) (C_ S T)) /edit/peano_new/set.gh/seqss, but S is not a proper subset of T. Subset is defined as (<-> (C_ S T) (=_ (i^i S T) S)) /edit/peano_new/set_min.ghi/df-ss.