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