. Sets
This introduces set theory from the point of view of a computer
professional using ASCII.
For the traditional notation see
.See http://www.math.csusb.edu/notes/sets/sets.html

For any type T there is an another type (symbolized by @T) of objects
that are sets of objects of type T.  For example {1,2,3} is a set of
type @Nat because 1, 2 and 3 are of type Nat.

The subsets of a given type are not (in MATHS) a type. However a set
does belong to a particular type: a set A is of type @T if and only if
A's elements must be of type T.  It is therefore
unambiguous to use the symbol/name for the type to be the universal set
of that type.

The main expressions involving sets in MATHS are:

.As_is	Expression	Meaning		Type.
.As_is ------------------------------------------------------------------
.As_is	{},$()		null set	Overloaded
.As_is	T		universal set	@T
.As_is	@T		Sets of elements of type T	@@T
.As_is	{e1},$(e1)	singleton	@T
.As_is				where e1 is of type T

.As_is	{e1,e2,e3,...}	extension	@T
.As_is	$(e1,e2,...)	extension	@T
.As_is				where e1,e2 ,e3,... are all of type T

.As_is	{x:T || W(x) }	intension	@T
.As_is	$[x:T](W(x))	intension	@T
There is a newer form:
.As_is 	set{x:T. W(x)}	intension	@T

.As_is	e1 in  S1	membership	T><@T  -> @

.As_is	S1 & S2		intersection	@T><@T -> @T(serial)
.As_is	S1 | S2		union		@T><@T -> @T(serial)
.As_is	S1 ~ S2		complement	@T><@T -> @T

.As_is	S1<> S2		inequality	@T><@T -> @(parallel operator)
.As_is	S1 =  S2	equality	@T><@T -> @(parallel operator)
.As_is	S1==>S2		subset or equal	@T><@T -> @(parallel operator)
.As_is	S1=>>S2		subset         	@T><@T -> @(parallel operator)
.As_is	S1>==S2		Partition      	@T><@@T ->@(parallel operator)
.As_is	S1		non-empty set	@ (overloaded)
.As_is	SetOf(S)	@S	@@T
.As_is	S@n	Subsets of size n	@@T
.As_is ------------------------------------------------------------------
The '$' (currency symbol) is a theoretical notation, the braces are 
a traditional shorthand.  SetOf spells out the meaning of "@".

Sample of Assumed Properties
	|- For x:T, x in T and not x in {}
	|- For e:T, e in {e} and e in {...,e,...} and e in {x:T||W(x)} iff W(e).

Note. The
.As_is 	|-
symbol marks a statement that is asserted as being true - either
as an axiom, or because it can be proved from other assertions.

Definitions of Set Operations
	A & B::={c || c in A and c in B},
	A | B::={c || c in A or c in B},
	A ~ B::={c || c in A and not( c in B) },

Definitions of relationships
	|- For A,B, A = B iff A==>B and B==>A,
	For A,B, A==>B::= for all a:A(a in B),
	For A,B, A=>>B::= A==>B and not A=B.

	For A,B, A>==B::=( |B=A and for all X,Y:B(X=Y or X&Y={}) ),
	For A,B, A>==B iff for all a:A, one X in B(a in X).

Useful abbreviations
	For A:Sets, a:Elements, A|a::=A|{a},
	a|A::={a}|A,
	etc.

Cardinallity -- size of a set
	|A| ::Nat0= `the number of elements in A`.
	A@n ::@A=`subsets of n elements taken from set A`