Reqmnts, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Basic Properties of Subsets --- Requirements

**by****Library Committee**- Received February 27, 2003
- MML identifier: SUBSET

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE; notation TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1; constructors TARSKI, SUBSET_1, XBOOLE_0; clusters SUBSET_1, ZFMISC_1, XBOOLE_0; begin :: This file contains statements which are obvious for Mizar checker if :: "requirements SUBSET" is included in the environment description :: of an article. They are published for testing purposes only. :: Users should use appropriate requirements instead of referencing :: to these theorems. :: Some of these items need also "requirements BOOLE" for proper work. theorem :: SUBSET:1 for a, b being set holds a in b implies a is Element of b; theorem :: SUBSET:2 :: requirements BOOLE also needed for a, b being set holds a is Element of b & b is non empty implies a in b; theorem :: SUBSET:3 for a, b being set holds a is Element of bool b iff a c= b; theorem :: SUBSET:4 for a, b, c being set holds a in b & b is Element of bool c implies a is Element of c; theorem :: SUBSET:5 :: requirements BOOLE also needed for a, b, c being set holds a in b & b is Element of bool c implies c is non empty;

Back to top