:: Basic Properties of Subsets - Requirements :: by Library Committee :: :: Received February 27, 2003 :: Copyright (c) 2003-2017 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;