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;