:: by Zinaida Trybulec

::

:: Received March 4, 1989

:: Copyright (c) 1990-2017 Association of Mizar Users

registration
end;

registration

let x1, x2, x3 be object ;

coherence

not {x1,x2,x3} is empty by ENUMSET1:def 1;

let x4 be object ;

coherence

not {x1,x2,x3,x4} is empty by ENUMSET1:def 2;

let x5 be object ;

coherence

not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def 3;

let x6 be object ;

coherence

not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def 4;

let x7 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def 5;

let x8 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def 6;

let x9 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def 7;

let x10 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def 8;

end;
coherence

not {x1,x2,x3} is empty by ENUMSET1:def 1;

let x4 be object ;

coherence

not {x1,x2,x3,x4} is empty by ENUMSET1:def 2;

let x5 be object ;

coherence

not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def 3;

let x6 be object ;

coherence

not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def 4;

let x7 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def 5;

let x8 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def 6;

let x9 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def 7;

let x10 be object ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def 8;

definition

let X be set ;

( ( not X is empty implies ex b_{1} being set st b_{1} in X ) & ( X is empty implies ex b_{1} being set st b_{1} is empty ) )

for b_{1} being set holds verum
;

sethood

( ( not X is empty & ex b_{1} being set st

for b_{2} being set st b_{2} in X holds

b_{2} in b_{1} ) or ( X is empty & ex b_{1} being set st

for b_{2} being set st b_{2} is empty holds

b_{2} in b_{1} ) )

end;
mode Element of X -> set means :Def1: :: SUBSET_1:def 1

it in X if not X is empty

otherwise it is empty ;

existence it in X if not X is empty

otherwise it is empty ;

( ( not X is empty implies ex b

proof end;

consistency for b

sethood

( ( not X is empty & ex b

for b

b

for b

b

proof end;

:: deftheorem Def1 defines Element SUBSET_1:def 1 :

for X, b_{2} being set holds

( ( not X is empty implies ( b_{2} is Element of X iff b_{2} in X ) ) & ( X is empty implies ( b_{2} is Element of X iff b_{2} is empty ) ) );

for X, b

( ( not X is empty implies ( b

registration
end;

definition

let D be non empty set ;

let X be non empty Subset of D;

:: original: Element

redefine mode Element of X -> Element of D;

coherence

for b_{1} being Element of X holds b_{1} is Element of D

end;
let X be non empty Subset of D;

:: original: Element

redefine mode Element of X -> Element of D;

coherence

for b

proof end;

Lm1: for E being set

for X being Subset of E

for x being object st x in X holds

x in E

proof end;

definition

let E be set ;

coherence

{} is Subset of E

;

coherence

E is Subset of E

;

end;
coherence

{} is Subset of E

proof end;

correctness ;

coherence

E is Subset of E

proof end;

correctness ;

theorem Th2: :: SUBSET_1:2

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

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

proof end;

theorem :: SUBSET_1:3

definition

let E be set ;

let A be Subset of E;

coherence

E \ A is Subset of E

;

involutiveness

for b_{1}, b_{2} being Subset of E st b_{1} = E \ b_{2} holds

b_{2} = E \ b_{1}

:: original: \/

redefine func A \/ B -> Subset of E;

coherence

A \/ B is Subset of E

redefine func A \+\ B -> Subset of E;

coherence

A \+\ B is Subset of E

end;
let A be Subset of E;

coherence

E \ A is Subset of E

proof end;

correctness ;

involutiveness

for b

b

proof end;

let B be Subset of E;:: original: \/

redefine func A \/ B -> Subset of E;

coherence

A \/ B is Subset of E

proof end;

:: original: \+\redefine func A \+\ B -> Subset of E;

coherence

A \+\ B is Subset of E

proof end;

definition

let X, Y be set ;

:: original: \

redefine func X \ Y -> Subset of X;

coherence

X \ Y is Subset of X

end;
:: original: \

redefine func X \ Y -> Subset of X;

coherence

X \ Y is Subset of X

proof end;

definition

let E be set ;

let A be Subset of E;

let X be set ;

:: original: \

redefine func A \ X -> Subset of E;

coherence

A \ X is Subset of E

end;
let A be Subset of E;

let X be set ;

:: original: \

redefine func A \ X -> Subset of E;

coherence

A \ X is Subset of E

proof end;

definition

let E be set ;

let A be Subset of E;

let X be set ;

:: original: /\

redefine func A /\ X -> Subset of E;

coherence

A /\ X is Subset of E

end;
let A be Subset of E;

let X be set ;

:: original: /\

redefine func A /\ X -> Subset of E;

coherence

A /\ X is Subset of E

proof end;

definition

let E, X be set ;

let A be Subset of E;

:: original: /\

redefine func X /\ A -> Subset of E;

coherence

X /\ A is Subset of E

end;
let A be Subset of E;

:: original: /\

redefine func X /\ A -> Subset of E;

coherence

X /\ A is Subset of E

proof end;

theorem :: SUBSET_1:5

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

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

proof end;

theorem :: SUBSET_1:6

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

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

proof end;

theorem :: SUBSET_1:7

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

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

proof end;

theorem :: SUBSET_1:8

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

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

proof end;

theorem :: SUBSET_1:18

theorem :: SUBSET_1:20

for E, X being set

for A being Subset of E st X c= A & X c= A ` holds

X = {} by XBOOLE_1:67, XBOOLE_1:79;

for A being Subset of E st X c= A & X c= A ` holds

X = {} by XBOOLE_1:67, XBOOLE_1:79;

theorem :: SUBSET_1:21

theorem :: SUBSET_1:22

theorem :: SUBSET_1:27

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

for A, B being Subset of E st ( for a being Element of A holds a in B ) holds

A c= B

proof end;

theorem :: SUBSET_1:29

for E being set st E <> {} holds

for B being Subset of E

for x being Element of E st not x in B holds

x in B `

for B being Subset of E

for x being Element of E st not x in B holds

x in B `

proof end;

theorem Th30: :: SUBSET_1:30

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 `

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 `

proof end;

theorem :: SUBSET_1:31

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 `

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 `

proof end;

theorem :: SUBSET_1:32

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 `

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 `

proof end;

theorem :: SUBSET_1:37

for X being set

for x1, x2, x3, x4, x5 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5} is Subset of X

for x1, x2, x3, x4, x5 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5} is Subset of X

proof end;

theorem :: SUBSET_1:38

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

for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6} is Subset of X

proof end;

theorem :: SUBSET_1:39

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

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

proof end;

theorem :: SUBSET_1:40

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

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

proof end;

definition

let X, Y be non empty set ;

:: original: misses

redefine pred X misses Y;

irreflexivity

for X being non empty set holds R6(b_{1},b_{1})
;

end;
:: original: misses

redefine pred X misses Y;

irreflexivity

for X being non empty set holds R6(b

definition

let X, Y be non empty set ;

:: original: misses

redefine pred X meets Y;

reflexivity

for X being non empty set holds R6(b_{1},b_{1})
;

end;
:: original: misses

redefine pred X meets Y;

reflexivity

for X being non empty set holds R6(b

definition
end;

Lm2: for X, Y being set st ( for x being object st x in X holds

x in Y ) holds

X is Subset of Y

proof end;

Lm3: for E being set

for A being Subset of E

for x being object st x in A holds

x is Element of E

proof end;

:: from FIN_TOPO, 2006.11.07. A.T.

:: from SGRAPH1, 2008.06.02

registration
end;

:: from TEX_2, 2006.06.18, A.T. (simplified)

:: deftheorem defines proper SUBSET_1:def 6 :

for E being set

for A being Subset of E holds

( A is proper iff A <> E );

for E being set

for A being Subset of E holds

( A is proper iff A <> E );

registration
end;

registration

let E be non empty set ;

coherence

for b_{1} being Subset of E st not b_{1} is proper holds

not b_{1} is empty
;

coherence

for b_{1} being Subset of E st b_{1} is empty holds

b_{1} is proper
;

end;
coherence

for b

not b

coherence

for b

b

registration
end;

registration
end;

:: from GRCAT_1, 2010.02.18, A.T.

theorem :: SUBSET_1:43

for X, Y, A, z being set st z in A & A c= [:X,Y:] holds

ex x being Element of X ex y being Element of Y st z = [x,y]

ex x being Element of X ex y being Element of Y st z = [x,y]

proof end;

:: from BORSUK_4, 2011.03.04, A.T.

theorem :: SUBSET_1:44

for X being non empty set

for A, B being non empty Subset of X st A c< B holds

ex p being Element of X st

( p in B & A c= B \ {p} )

for A, B being non empty Subset of X st A c< B holds

ex p being Element of X st

( p in B & A c= B \ {p} )

proof end;

definition

let X be set ;

compatibility

( X is trivial iff for x, y being Element of X holds x = y )

end;
compatibility

( X is trivial iff for x, y being Element of X holds x = y )

proof end;

:: deftheorem defines trivial SUBSET_1:def 7 :

for X being set holds

( X is trivial iff for x, y being Element of X holds x = y );

for X being set holds

( X is trivial iff for x, y being Element of X holds x = y );

registration

let X be non empty set ;

existence

ex b_{1} being Subset of X st

( not b_{1} is empty & b_{1} is trivial )

end;
existence

ex b

( not b

proof end;

registration
end;

registration

let X be non trivial set ;

existence

not for b_{1} being Subset of X holds b_{1} is trivial

end;
existence

not for b

proof end;

theorem :: SUBSET_1:45

for D being set

for A being Subset of D st not A is trivial holds

ex d1, d2 being Element of D st

( d1 in A & d2 in A & d1 <> d2 )

for A being Subset of D st not A is trivial holds

ex d1, d2 being Element of D st

( d1 in A & d2 in A & d1 <> d2 )

proof end;

:: from BORSUK_4, 2011.07.31, A.T.

theorem :: SUBSET_1:47

for X being non empty set

for A being non empty Subset of X st A is trivial holds

ex x being Element of X st A = {x}

for A being non empty Subset of X st A is trivial holds

ex x being Element of X st A = {x}

proof end;

definition

let x be object ;

let X be set ;

assume A1: x in X ;

correctness

coherence

x is Element of X;

end;
let X be set ;

assume A1: x in X ;

correctness

coherence

x is Element of X;

proof end;

:: deftheorem Def7 defines In SUBSET_1:def 8 :

for x being object

for X being set st x in X holds

In (x,X) = x;

for x being object

for X being set st x in X holds

In (x,X) = x;

registration
end;

:: from BORSUK_4, 2012.08.12, A.T.

theorem :: SUBSET_1:51

for T being non trivial set

for X being non trivial Subset of T

for p being set ex q being Element of T st

( q in X & q <> p )

for X being non trivial Subset of T

for p being set ex q being Element of T st

( q in X & q <> p )

proof end;

:: 2012.12.16, A.T.

:: ADDITIONAL THEOREMS

::