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

begin

theorem :: SUBSET:1

for a, b being set st a in b holds
a is Element of b by SUBSET_1:def 2;

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 2;

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 ;