% $Id: RelSet.lsl,v 1.2 2000/01/17 21:33:40 connolly Exp $
% larch Set trait is for finite sets

RelSet(E, C): trait
    includes
        Relation(E, C,
 	         __ \< __ \> __ for __ \langle __ \rangle __,
		 bot for \bot, top for \top)

    introduces
        { __ } : E -> C
        { } : -> C

    asserts
        \forall e1, e2: E
        (e1 \< { e2 } \> e1) = (e1=e2);
	e1 \notin {};