introduces:   set , element , set of _ . 

needs:        Tuples/Basics .  element <= component .
 set = set of element* .
 element = nonset-element | set  (disjoint) .
 set of _ :: element* -> set (total) . 
(1) set of (e:element*, e1:element, 
	e2:element, e':element*) = set of (e, e2, e1, e') .
(2) e1 is e2 = true =>  set of (e:element*, e1:element, e2:element, 
	e':element*) = set of (e, e1, e') .

closed except Generics .

introduces:  _ [ _ ] ,  elements _ , empty-set , disjoint-union _ , union _ , difference _ , intersection _ , _ restricted to _ ,
		 _ omitting _ , _ [in _ ] , _ [not in _] , _ is in _ , _ is included in _ . 

includes:   Instant/Partial Order ( set for s , _is_ , _ is included in _ for _ is less than _ ) .

needs:       Tuples, Lists .
 _ [ _ ] 		:: set, element -> set .
 elements _ 		:: ( set -> element* (strict, linear) .
 empty-set 		:  set .
 disjoint-union _ 	:: set* -> set  (partial, associative, commutative, unit is empty-set) . 
 union _ 		:: set* -> set  (total, associative, commutative, idempotent, unit is empty-set) . 
 difference _ 		:: set, set -> set (total) . 
 intersection _ 	:: set+ -> set  (total, associative, commutative, idempotent) . 
 _ restricted to _ 	:: list [element], set -> list [element] (total) . 
 _ omitting _ 		:: list [element], set -> list [element] (total) . 
 _ [in _ ]  		:: element, set -> element (partial) . 
 _ [not in _ ] 		:: element, set -> element (partial) . 
 _ is in _ 		:: element, set -> truth-value (total) . 
 _ is included in _ 	:: set, set -> truth-value (total) . 
 _is_ 			:: set, set -> truth-value (total) .
(1) (s <= set) [ e <= element ] = s & set of e* .
(2) s = set of e:element* ; distinct e = true => elements (s:set) = shuffle e .
(3) empty-set = set of ( ) .
(4) disjoint-union (s:set, t:set) = when intersection (s, t) is empty-set then union (s, t) .
(5) union (set of e1:element*, set of e2:element*) = set of (e1, e2) .
(6) difference (empty-set, s:set) = empty-set ;
	difference (s:set, empty-set) = s ;
	difference (set of e:element, s:set) = 
		if e is in s then empty-set else set of e ;
	difference (union (s:set, t:set), u':set) = 
		union (difference (s, u'), difference (t, u')) .
(7) intersection (empty-set, s:set) = empty-set ;
	intersection (set of e:element, s:set) =  if e is in s then set of e else empty-set ;
	intersection (union (s:set, t:set), u':set) =
		union (intersection (s, u'), intersection (t, u')) .
(8) empty-list restricted to s:set = empty-list ;
	empty-list omitting s:set = empty-list .
(9) concatenation (list of e:element, l:list) restricted to s:set = 
		if e is in s then concatenation (list of e, l restricted to s) 
			else l restricted to s ;   
	concatenation (list of e:element, l:list) omitting s:set = 
		if not (e is in s) then concatenation (list of e, l omitting s) 
			else l omitting s .
(10)(e:element) [in s:set]  = when e is in s then e ;
	(e:element) [not in s:set] e:element = when not (e is in s) then e .
(11)e:element is in empty-set = false ;
	e:element is in union (s:set, t:set) = either ((e is in s), (e is in t)) .
(12)s:set is included in t:set = union (s, t) is t .
(13)empty-set is set of e:element+ = false ;
	union (set of e:element, s:set) is t:set =
		both ((e is in t), (difference (s, set of e) is difference (t, set of e))) .