:: Basic Properties of Subsets - Requirements
::  by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, XBOOLE_0, TARSKI, ZFMISC_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1;
 constructors TARSKI, SUBSET_1;
 registrations SUBSET_1;
 requirements BOOLE;
 theorems TARSKI, 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
  for a, b being set st a in b holds a is Element of b by SUBSET_1:def 1;

theorem
  for a, b being set st a is Element of b & b is non empty holds a in b
  by SUBSET_1:def 1;

theorem Th3:
  for a, b being set holds a is Subset of b iff a c= b
proof
  let a, b be set;
  hereby
    assume a is Subset of b;
    then a in bool b by SUBSET_1:def 1;
    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 1;
end;

theorem
  for a, b, c being set st a in b & b is Subset of c holds a is Element of c
proof
  let a, b, c be set;
  assume that
A1: a in b and
A2: b is Subset of c;
  b c= c by A2,Th3;
  then a in c by A1,TARSKI:def 3;
  hence thesis by SUBSET_1:def 1;
end;

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