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

:: 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 )

proof end;

theorem :: SUBSET:4

for a, b, c being set st a in b & b is Subset of c holds
a is Element of c

proof end;

theorem :: SUBSET:5

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