-(* subset inclusion *)
-definition ssub: \forall D. Subset D \to Subset D \to Prop \def
- \lambda D,U1,U2. \forall d. U1 d \to U2 d.
+(* subset membership (epsilon) *)
+definition sin : \forall D. Subset D \to D \to Prop \def
+ \lambda (D:Domain). \lambda U,d. cin D d \and U d.
+
+(* subset top (full subset) *)
+definition stop \def \lambda (D:Domain). true_f D.
+
+(* subset bottom (empty subset) *)
+definition sbot \def \lambda (D:Domain). false_f D.
+
+(* subset and (binary intersection) *)
+definition sand: \forall D. Subset D \to Subset D \to Subset D \def
+ \lambda D,U1,U2,d. U1 d \land U2 d.