### The Mizar article:

### Basic Properties of Subsets --- Requirements

**by****Library Committee**

- Received February 27, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: SUBSET
- [ 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; theorems TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1; 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 Th1: for a, b being set holds a in b implies a is Element of b proof let a, b be set; assume A1: a in b; then b <> {} by XBOOLE_0:def 1; then b is non empty by XBOOLE_0:def 5; hence a is Element of b by A1,SUBSET_1:def 2; end; theorem :: requirements BOOLE also needed for a, b being set holds a is Element of b & b is non empty implies a in b by SUBSET_1:def 2; theorem Th3: for a, b being set holds a is Element of bool b iff a c= b proof let a, b be set; hereby assume a is Element of bool b; then a in bool b by SUBSET_1:def 2; hence a c= b by ZFMISC_1:def 1; end; assume a c= b; then a in bool b by ZFMISC_1:def 1; hence thesis by SUBSET_1:def 2; end; theorem for a, b, c being set holds a in b & b is Element of bool c implies a is Element of c proof let a, b, c be set; assume that A1: a in b and A2: b is Element of bool c; b c= c by A2,Th3; then a in c by A1,TARSKI:def 3; hence a is Element of c by Th1; end; theorem :: 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 proof let a, b, c be set; assume that A1: a in b and A2: b is Element of bool c; b c= c by A2,Th3; then a in c by A1,TARSKI:def 3; then c <> {} by XBOOLE_0:def 1; hence c is non empty by XBOOLE_0:def 5; end;

Back to top