:: Basic Properties of Subsets - Requirements
:: by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


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 st a in b holds
a is Element of b by SUBSET_1:def_1;

theorem :: SUBSET:2
for a, b being set st a is Element of b & not b is empty holds
a in b by SUBSET_1:def_1;

theorem Th3: :: SUBSET:3
for a, b being set holds
( a is Subset of b iff a c= b )
proofend;

theorem :: SUBSET:4
for a, b, c being set st a in b & b is Subset of c holds
a is Element of c
proofend;

theorem :: SUBSET:5
for a, b, c being set st a in b & b is Subset of c holds
not c is empty ;