COMPRELN.TXT          1995 September 12

The CR group of theorems is concerned with the concept of
complementary relation, defined by

equal(restrict(complement(x),V,V),compreln(x)).

The concept of complementary relation figures prominently in
Tarski and Givant's book.  It is one of their four primitive
operators, introduced on page 23.

Alfred Tarski and Steven Givant, "A Formalization of Set Theory
without Variables," American Mathematical Society Colloquium
Publications, volume 41, Providence, Rhode Island, 1987.


It has not been decided yet whether to retain this group of theorems
permanently on the usable list, but in any case, there are some
features of interest worth noting.  The strategy used to prove the
theorems of the CR group is quite similar to that used for the group
RC which deals with relative complements. In most of these theorems,
we could get by with very few weight settings, and in many instances
only para_into was needed.  Clearing the flag para_into_right helped
in several cases.

If we do decide to keep this group of theorems, it could be placed
immediately following the two groups RS and DJ, which deal with the
restriction functor restrict(*,*,*) and the predicate disjoint(*,*),
respectively.