for Y being non empty set holds '/\' ({} (PARTITIONS Y)) = %O Y