:: Properties of Subsets
:: by Zinaida Trybulec
::
:: Received March 4, 1989
:: Copyright (c) 1990 Association of Mizar Users
registration
let x1,
x2,
x3 be
set ;
cluster {x1,x2,x3} -> non
empty ;
coherence
not {x1,x2,x3} is empty
by ENUMSET1:def 1;
let x4 be
set ;
cluster {x1,x2,x3,x4} -> non
empty ;
coherence
not {x1,x2,x3,x4} is empty
by ENUMSET1:def 2;
let x5 be
set ;
cluster {x1,x2,x3,x4,x5} -> non
empty ;
coherence
not {x1,x2,x3,x4,x5} is empty
by ENUMSET1:def 3;
let x6 be
set ;
cluster {x1,x2,x3,x4,x5,x6} -> non
empty ;
coherence
not {x1,x2,x3,x4,x5,x6} is empty
by ENUMSET1:def 4;
let x7 be
set ;
cluster {x1,x2,x3,x4,x5,x6,x7} -> non
empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7} is empty
by ENUMSET1:def 5;
let x8 be
set ;
cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> non
empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7,x8} is empty
by ENUMSET1:def 6;
let x9 be
set ;
cluster {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> non
empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty
by ENUMSET1:def 7;
let x10 be
set ;
cluster {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> non
empty ;
coherence
not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty
by ENUMSET1:def 8;
end;
:: deftheorem SUBSET_1:def 1 :
canceled;
:: deftheorem Def2 defines Element SUBSET_1:def 2 :
Lm1:
for E being set
for X being Subset of E
for x being set st x in X holds
x in E
:: deftheorem defines {} SUBSET_1:def 3 :
:: deftheorem defines [#] SUBSET_1:def 4 :
theorem :: SUBSET_1:1
canceled;
theorem :: SUBSET_1:2
canceled;
theorem :: SUBSET_1:3
canceled;
theorem :: SUBSET_1:4
theorem :: SUBSET_1:5
canceled;
theorem :: SUBSET_1:6
canceled;
theorem Th7: :: SUBSET_1:7
for
E being
set for
A,
B being
Subset of
E st ( for
x being
Element of
E st
x in A holds
x in B ) holds
A c= B
theorem Th8: :: SUBSET_1:8
for
E being
set for
A,
B being
Subset of
E st ( for
x being
Element of
E holds
(
x in A iff
x in B ) ) holds
A = B
theorem :: SUBSET_1:9
canceled;
theorem :: SUBSET_1:10
:: deftheorem defines ` SUBSET_1:def 5 :
theorem :: SUBSET_1:11
canceled;
theorem :: SUBSET_1:12
canceled;
theorem :: SUBSET_1:13
canceled;
theorem :: SUBSET_1:14
canceled;
theorem :: SUBSET_1:15
for
E being
set for
A,
B,
C being
Subset of
E st ( for
x being
Element of
E holds
(
x in A iff (
x in B or
x in C ) ) ) holds
A = B \/ C
theorem :: SUBSET_1:16
for
E being
set for
A,
B,
C being
Subset of
E st ( for
x being
Element of
E holds
(
x in A iff (
x in B &
x in C ) ) ) holds
A = B /\ C
theorem :: SUBSET_1:17
for
E being
set for
A,
B,
C being
Subset of
E st ( for
x being
Element of
E holds
(
x in A iff (
x in B & not
x in C ) ) ) holds
A = B \ C
theorem :: SUBSET_1:18
for
E being
set for
A,
B,
C being
Subset of
E st ( for
x being
Element of
E holds
(
x in A iff ( (
x in B & not
x in C ) or (
x in C & not
x in B ) ) ) ) holds
A = B \+\ C
theorem :: SUBSET_1:19
canceled;
theorem :: SUBSET_1:20
canceled;
theorem :: SUBSET_1:21
canceled;
theorem :: SUBSET_1:22
theorem :: SUBSET_1:23
canceled;
theorem :: SUBSET_1:24
canceled;
theorem Th25: :: SUBSET_1:25
theorem :: SUBSET_1:26
canceled;
theorem :: SUBSET_1:27
canceled;
theorem :: SUBSET_1:28
theorem :: SUBSET_1:29
canceled;
theorem :: SUBSET_1:30
canceled;
theorem Th31: :: SUBSET_1:31
theorem :: SUBSET_1:32
theorem :: SUBSET_1:33
theorem :: SUBSET_1:34
theorem :: SUBSET_1:35
theorem :: SUBSET_1:36
theorem :: SUBSET_1:37
canceled;
theorem :: SUBSET_1:38
theorem :: SUBSET_1:39
theorem :: SUBSET_1:40
theorem :: SUBSET_1:41
theorem :: SUBSET_1:42
theorem Th43: :: SUBSET_1:43
theorem :: SUBSET_1:44
theorem :: SUBSET_1:45
canceled;
theorem :: SUBSET_1:46
theorem :: SUBSET_1:47
theorem :: SUBSET_1:48
for
E being
set for
A,
B being
Subset of
E st ( for
a being
Element of
A holds
a in B ) holds
A c= B
theorem :: SUBSET_1:49
for
E being
set for
A being
Subset of
E st ( for
x being
Element of
E holds
x in A ) holds
E = A
theorem :: SUBSET_1:50
theorem Th51: :: SUBSET_1:51
for
E being
set for
A,
B being
Subset of
E st ( for
x being
Element of
E holds
(
x in A iff not
x in B ) ) holds
A = B `
theorem :: SUBSET_1:52
for
E being
set for
A,
B being
Subset of
E st ( for
x being
Element of
E holds
( not
x in A iff
x in B ) ) holds
A = B `
theorem :: SUBSET_1:53
for
E being
set for
A,
B being
Subset of
E st ( for
x being
Element of
E holds
( (
x in A & not
x in B ) or (
x in B & not
x in A ) ) ) holds
A = B `
theorem :: SUBSET_1:54
canceled;
theorem :: SUBSET_1:55
theorem :: SUBSET_1:56
theorem :: SUBSET_1:57
theorem :: SUBSET_1:58
theorem :: SUBSET_1:59
theorem :: SUBSET_1:60
for
X being
set for
x1,
x2,
x3,
x4,
x5,
x6 being
Element of
X st
X <> {} holds
{x1,x2,x3,x4,x5,x6} is
Subset of
X
theorem :: SUBSET_1:61
for
X being
set for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
Element of
X st
X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is
Subset of
X
theorem :: SUBSET_1:62
for
X being
set for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
Element of
X st
X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8} is
Subset of
X
theorem :: SUBSET_1:63
:: deftheorem defines choose SUBSET_1:def 6 :
Lm2:
for X, Y being set st ( for x being set st x in X holds
x in Y ) holds
X is Subset of Y
Lm3:
for x, E being set
for A being Subset of E st x in A holds
x is Element of E
theorem :: SUBSET_1:64
for
E being
set for
A,
B being
Subset of
E st
A ` = B ` holds
A = B
:: deftheorem defines proper SUBSET_1:def 7 :