for W being Universe holds
( 0-element_of W = {} & 1-element_of W = 1 ) ;