:: by Andrzej Trybulec

::

:: Received August 23, 2003

:: Copyright (c) 2003-2012 Association of Mizar Users

begin

definition

let X be set ;

end;
attr X is complex-membered means :Def1: :: MEMBERED:def 1

for x being set st x in X holds

x is complex ;

for x being set st x in X holds

x is complex ;

attr X is ext-real-membered means :Def2: :: MEMBERED:def 2

for x being set st x in X holds

x is ext-real ;

for x being set st x in X holds

x is ext-real ;

attr X is rational-membered means :Def4: :: MEMBERED:def 4

for x being set st x in X holds

x is rational ;

for x being set st x in X holds

x is rational ;

attr X is integer-membered means :Def5: :: MEMBERED:def 5

for x being set st x in X holds

x is integer ;

for x being set st x in X holds

x is integer ;

attr X is natural-membered means :Def6: :: MEMBERED:def 6

for x being set st x in X holds

x is natural ;

for x being set st x in X holds

x is natural ;

:: deftheorem Def1 defines complex-membered MEMBERED:def 1 :

for X being set holds

( X is complex-membered iff for x being set st x in X holds

x is complex );

for X being set holds

( X is complex-membered iff for x being set st x in X holds

x is complex );

:: deftheorem Def2 defines ext-real-membered MEMBERED:def 2 :

for X being set holds

( X is ext-real-membered iff for x being set st x in X holds

x is ext-real );

for X being set holds

( X is ext-real-membered iff for x being set st x in X holds

x is ext-real );

:: deftheorem Def3 defines real-membered MEMBERED:def 3 :

for X being set holds

( X is real-membered iff for x being set st x in X holds

x is real );

for X being set holds

( X is real-membered iff for x being set st x in X holds

x is real );

:: deftheorem Def4 defines rational-membered MEMBERED:def 4 :

for X being set holds

( X is rational-membered iff for x being set st x in X holds

x is rational );

for X being set holds

( X is rational-membered iff for x being set st x in X holds

x is rational );

:: deftheorem Def5 defines integer-membered MEMBERED:def 5 :

for X being set holds

( X is integer-membered iff for x being set st x in X holds

x is integer );

for X being set holds

( X is integer-membered iff for x being set st x in X holds

x is integer );

:: deftheorem Def6 defines natural-membered MEMBERED:def 6 :

for X being set holds

( X is natural-membered iff for x being set st x in X holds

x is natural );

for X being set holds

( X is natural-membered iff for x being set st x in X holds

x is natural );

registration

coherence

for b_{1} being set st b_{1} is natural-membered holds

b_{1} is integer-membered

for b_{1} being set st b_{1} is integer-membered holds

b_{1} is rational-membered

for b_{1} being set st b_{1} is rational-membered holds

b_{1} is real-membered

for b_{1} being set st b_{1} is real-membered holds

b_{1} is ext-real-membered

for b_{1} being set st b_{1} is real-membered holds

b_{1} is complex-membered

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration

coherence

for b_{1} being Subset of COMPLEX holds b_{1} is complex-membered

for b_{1} being Subset of ExtREAL holds b_{1} is ext-real-membered

for b_{1} being Subset of REAL holds b_{1} is real-membered

for b_{1} being Subset of RAT holds b_{1} is rational-membered

for b_{1} being Subset of INT holds b_{1} is integer-membered

for b_{1} being Subset of NAT holds b_{1} is natural-membered

end;
for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

registration

coherence

COMPLEX is complex-membered

ExtREAL is ext-real-membered

REAL is real-membered

RAT is rational-membered

INT is integer-membered

NAT is natural-membered

end;
COMPLEX is complex-membered

proof end;

coherence ExtREAL is ext-real-membered

proof end;

coherence REAL is real-membered

proof end;

coherence RAT is rational-membered

proof end;

coherence INT is integer-membered

proof end;

coherence NAT is natural-membered

proof end;

registration

let X be complex-membered set ;

coherence

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

end;
coherence

for b

proof end;

registration

let X be ext-real-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is ext-real

end;
coherence

for b

proof end;

registration
end;

registration

let X be rational-membered set ;

coherence

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

end;
coherence

for b

proof end;

registration

let X be integer-membered set ;

coherence

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

end;
coherence

for b

proof end;

registration

let X be natural-membered set ;

coherence

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

end;
coherence

for b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let X be complex-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is complex-membered

end;
coherence

for b

proof end;

registration

let X be ext-real-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is ext-real-membered

end;
coherence

for b

proof end;

registration

let X be real-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is real-membered

end;
coherence

for b

proof end;

registration

let X be rational-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is rational-membered

end;
coherence

for b

proof end;

registration

let X be integer-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is integer-membered

end;
coherence

for b

proof end;

registration

let X be natural-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is natural-membered

end;
coherence

for b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let X be complex-membered set ;

let Y be set ;

coherence

X /\ Y is complex-membered by Th19, XBOOLE_1:17;

coherence

Y /\ X is complex-membered ;

end;
let Y be set ;

coherence

X /\ Y is complex-membered by Th19, XBOOLE_1:17;

coherence

Y /\ X is complex-membered ;

registration

let X be ext-real-membered set ;

let Y be set ;

coherence

X /\ Y is ext-real-membered by Th20, XBOOLE_1:17;

coherence

Y /\ X is ext-real-membered ;

end;
let Y be set ;

coherence

X /\ Y is ext-real-membered by Th20, XBOOLE_1:17;

coherence

Y /\ X is ext-real-membered ;

registration

let X be real-membered set ;

let Y be set ;

coherence

X /\ Y is real-membered by Th21, XBOOLE_1:17;

coherence

Y /\ X is real-membered ;

end;
let Y be set ;

coherence

X /\ Y is real-membered by Th21, XBOOLE_1:17;

coherence

Y /\ X is real-membered ;

registration

let X be rational-membered set ;

let Y be set ;

coherence

X /\ Y is rational-membered by Th22, XBOOLE_1:17;

coherence

Y /\ X is rational-membered ;

end;
let Y be set ;

coherence

X /\ Y is rational-membered by Th22, XBOOLE_1:17;

coherence

Y /\ X is rational-membered ;

registration

let X be integer-membered set ;

let Y be set ;

coherence

X /\ Y is integer-membered by Th23, XBOOLE_1:17;

coherence

Y /\ X is integer-membered ;

end;
let Y be set ;

coherence

X /\ Y is integer-membered by Th23, XBOOLE_1:17;

coherence

Y /\ X is integer-membered ;

registration

let X be natural-membered set ;

let Y be set ;

coherence

X /\ Y is natural-membered by Th24, XBOOLE_1:17;

coherence

Y /\ X is natural-membered ;

end;
let Y be set ;

coherence

X /\ Y is natural-membered by Th24, XBOOLE_1:17;

coherence

Y /\ X is natural-membered ;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

definition

let X be complex-membered set ;

let Y be set ;

( X c= Y iff for c being complex number st c in X holds

c in Y )

end;
let Y be set ;

redefine pred X c= Y means :Def7: :: MEMBERED:def 7

for c being complex number st c in X holds

c in Y;

compatibility for c being complex number st c in X holds

c in Y;

( X c= Y iff for c being complex number st c in X holds

c in Y )

proof end;

:: deftheorem Def7 defines c= MEMBERED:def 7 :

for X being complex-membered set

for Y being set holds

( X c= Y iff for c being complex number st c in X holds

c in Y );

for X being complex-membered set

for Y being set holds

( X c= Y iff for c being complex number st c in X holds

c in Y );

definition

let X be ext-real-membered set ;

let Y be set ;

( X c= Y iff for e being ext-real number st e in X holds

e in Y )

end;
let Y be set ;

redefine pred X c= Y means :Def8: :: MEMBERED:def 8

for e being ext-real number st e in X holds

e in Y;

compatibility for e being ext-real number st e in X holds

e in Y;

( X c= Y iff for e being ext-real number st e in X holds

e in Y )

proof end;

:: deftheorem Def8 defines c= MEMBERED:def 8 :

for X being ext-real-membered set

for Y being set holds

( X c= Y iff for e being ext-real number st e in X holds

e in Y );

for X being ext-real-membered set

for Y being set holds

( X c= Y iff for e being ext-real number st e in X holds

e in Y );

definition

let X be real-membered set ;

let Y be set ;

compatibility

( X c= Y iff for r being real number st r in X holds

r in Y )

end;
let Y be set ;

compatibility

( X c= Y iff for r being real number st r in X holds

r in Y )

proof end;

:: deftheorem Def9 defines c= MEMBERED:def 9 :

for X being real-membered set

for Y being set holds

( X c= Y iff for r being real number st r in X holds

r in Y );

for X being real-membered set

for Y being set holds

( X c= Y iff for r being real number st r in X holds

r in Y );

definition

let X be rational-membered set ;

let Y be set ;

( X c= Y iff for w being rational number st w in X holds

w in Y )

end;
let Y be set ;

redefine pred X c= Y means :Def10: :: MEMBERED:def 10

for w being rational number st w in X holds

w in Y;

compatibility for w being rational number st w in X holds

w in Y;

( X c= Y iff for w being rational number st w in X holds

w in Y )

proof end;

:: deftheorem Def10 defines c= MEMBERED:def 10 :

for X being rational-membered set

for Y being set holds

( X c= Y iff for w being rational number st w in X holds

w in Y );

for X being rational-membered set

for Y being set holds

( X c= Y iff for w being rational number st w in X holds

w in Y );

definition

let X be integer-membered set ;

let Y be set ;

( X c= Y iff for i being integer number st i in X holds

i in Y )

end;
let Y be set ;

redefine pred X c= Y means :Def11: :: MEMBERED:def 11

for i being integer number st i in X holds

i in Y;

compatibility for i being integer number st i in X holds

i in Y;

( X c= Y iff for i being integer number st i in X holds

i in Y )

proof end;

:: deftheorem Def11 defines c= MEMBERED:def 11 :

for X being integer-membered set

for Y being set holds

( X c= Y iff for i being integer number st i in X holds

i in Y );

for X being integer-membered set

for Y being set holds

( X c= Y iff for i being integer number st i in X holds

i in Y );

definition

let X be natural-membered set ;

let Y be set ;

compatibility

( X c= Y iff for n being Nat st n in X holds

n in Y )

end;
let Y be set ;

compatibility

( X c= Y iff for n being Nat st n in X holds

n in Y )

proof end;

:: deftheorem Def12 defines c= MEMBERED:def 12 :

for X being natural-membered set

for Y being set holds

( X c= Y iff for n being Nat st n in X holds

n in Y );

for X being natural-membered set

for Y being set holds

( X c= Y iff for n being Nat st n in X holds

n in Y );

definition

let X, Y be complex-membered set ;

( X = Y iff for c being complex number holds

( c in X iff c in Y ) )

end;
redefine pred X = Y means :: MEMBERED:def 13

for c being complex number holds

( c in X iff c in Y );

compatibility for c being complex number holds

( c in X iff c in Y );

( X = Y iff for c being complex number holds

( c in X iff c in Y ) )

proof end;

:: deftheorem defines = MEMBERED:def 13 :

for X, Y being complex-membered set holds

( X = Y iff for c being complex number holds

( c in X iff c in Y ) );

for X, Y being complex-membered set holds

( X = Y iff for c being complex number holds

( c in X iff c in Y ) );

definition

let X, Y be ext-real-membered set ;

( X = Y iff for e being ext-real number holds

( e in X iff e in Y ) )

end;
redefine pred X = Y means :: MEMBERED:def 14

for e being ext-real number holds

( e in X iff e in Y );

compatibility for e being ext-real number holds

( e in X iff e in Y );

( X = Y iff for e being ext-real number holds

( e in X iff e in Y ) )

proof end;

:: deftheorem defines = MEMBERED:def 14 :

for X, Y being ext-real-membered set holds

( X = Y iff for e being ext-real number holds

( e in X iff e in Y ) );

for X, Y being ext-real-membered set holds

( X = Y iff for e being ext-real number holds

( e in X iff e in Y ) );

definition

let X, Y be real-membered set ;

compatibility

( X = Y iff for r being real number holds

( r in X iff r in Y ) )

end;
compatibility

( X = Y iff for r being real number holds

( r in X iff r in Y ) )

proof end;

:: deftheorem defines = MEMBERED:def 15 :

for X, Y being real-membered set holds

( X = Y iff for r being real number holds

( r in X iff r in Y ) );

for X, Y being real-membered set holds

( X = Y iff for r being real number holds

( r in X iff r in Y ) );

definition

let X, Y be rational-membered set ;

( X = Y iff for w being rational number holds

( w in X iff w in Y ) )

end;
redefine pred X = Y means :: MEMBERED:def 16

for w being rational number holds

( w in X iff w in Y );

compatibility for w being rational number holds

( w in X iff w in Y );

( X = Y iff for w being rational number holds

( w in X iff w in Y ) )

proof end;

:: deftheorem defines = MEMBERED:def 16 :

for X, Y being rational-membered set holds

( X = Y iff for w being rational number holds

( w in X iff w in Y ) );

for X, Y being rational-membered set holds

( X = Y iff for w being rational number holds

( w in X iff w in Y ) );

definition

let X, Y be integer-membered set ;

( X = Y iff for i being integer number holds

( i in X iff i in Y ) )

end;
redefine pred X = Y means :: MEMBERED:def 17

for i being integer number holds

( i in X iff i in Y );

compatibility for i being integer number holds

( i in X iff i in Y );

( X = Y iff for i being integer number holds

( i in X iff i in Y ) )

proof end;

:: deftheorem defines = MEMBERED:def 17 :

for X, Y being integer-membered set holds

( X = Y iff for i being integer number holds

( i in X iff i in Y ) );

for X, Y being integer-membered set holds

( X = Y iff for i being integer number holds

( i in X iff i in Y ) );

definition

let X, Y be natural-membered set ;

compatibility

( X = Y iff for n being Nat holds

( n in X iff n in Y ) )

end;
compatibility

( X = Y iff for n being Nat holds

( n in X iff n in Y ) )

proof end;

:: deftheorem defines = MEMBERED:def 18 :

for X, Y being natural-membered set holds

( X = Y iff for n being Nat holds

( n in X iff n in Y ) );

for X, Y being natural-membered set holds

( X = Y iff for n being Nat holds

( n in X iff n in Y ) );

definition

let X, Y be complex-membered set ;

( not X meets Y iff for c being complex number holds

( not c in X or not c in Y ) )

end;
redefine pred X misses Y means :: MEMBERED:def 19

for c being complex number holds

( not c in X or not c in Y );

compatibility for c being complex number holds

( not c in X or not c in Y );

( not X meets Y iff for c being complex number holds

( not c in X or not c in Y ) )

proof end;

:: deftheorem defines meets MEMBERED:def 19 :

for X, Y being complex-membered set holds

( not X meets Y iff for c being complex number holds

( not c in X or not c in Y ) );

for X, Y being complex-membered set holds

( not X meets Y iff for c being complex number holds

( not c in X or not c in Y ) );

definition

let X, Y be ext-real-membered set ;

( not X meets Y iff for e being ext-real number holds

( not e in X or not e in Y ) )

end;
redefine pred X misses Y means :: MEMBERED:def 20

for e being ext-real number holds

( not e in X or not e in Y );

compatibility for e being ext-real number holds

( not e in X or not e in Y );

( not X meets Y iff for e being ext-real number holds

( not e in X or not e in Y ) )

proof end;

:: deftheorem defines meets MEMBERED:def 20 :

for X, Y being ext-real-membered set holds

( not X meets Y iff for e being ext-real number holds

( not e in X or not e in Y ) );

for X, Y being ext-real-membered set holds

( not X meets Y iff for e being ext-real number holds

( not e in X or not e in Y ) );

definition

let X, Y be real-membered set ;

( not X meets Y iff for r being real number holds

( not r in X or not r in Y ) )

end;
redefine pred X misses Y means :: MEMBERED:def 21

for r being real number holds

( not r in X or not r in Y );

compatibility for r being real number holds

( not r in X or not r in Y );

( not X meets Y iff for r being real number holds

( not r in X or not r in Y ) )

proof end;

:: deftheorem defines meets MEMBERED:def 21 :

for X, Y being real-membered set holds

( not X meets Y iff for r being real number holds

( not r in X or not r in Y ) );

for X, Y being real-membered set holds

( not X meets Y iff for r being real number holds

( not r in X or not r in Y ) );

definition

let X, Y be rational-membered set ;

( not X meets Y iff for w being rational number holds

( not w in X or not w in Y ) )

end;
redefine pred X misses Y means :: MEMBERED:def 22

for w being rational number holds

( not w in X or not w in Y );

compatibility for w being rational number holds

( not w in X or not w in Y );

( not X meets Y iff for w being rational number holds

( not w in X or not w in Y ) )

proof end;

:: deftheorem defines meets MEMBERED:def 22 :

for X, Y being rational-membered set holds

( not X meets Y iff for w being rational number holds

( not w in X or not w in Y ) );

for X, Y being rational-membered set holds

( not X meets Y iff for w being rational number holds

( not w in X or not w in Y ) );

definition

let X, Y be integer-membered set ;

( not X meets Y iff for i being integer number holds

( not i in X or not i in Y ) )

end;
redefine pred X misses Y means :: MEMBERED:def 23

for i being integer number holds

( not i in X or not i in Y );

compatibility for i being integer number holds

( not i in X or not i in Y );

( not X meets Y iff for i being integer number holds

( not i in X or not i in Y ) )

proof end;

:: deftheorem defines meets MEMBERED:def 23 :

for X, Y being integer-membered set holds

( not X meets Y iff for i being integer number holds

( not i in X or not i in Y ) );

for X, Y being integer-membered set holds

( not X meets Y iff for i being integer number holds

( not i in X or not i in Y ) );

definition

let X, Y be natural-membered set ;

( not X meets Y iff for n being Nat holds

( not n in X or not n in Y ) )

end;
redefine pred X misses Y means :: MEMBERED:def 24

for n being Nat holds

( not n in X or not n in Y );

compatibility for n being Nat holds

( not n in X or not n in Y );

( not X meets Y iff for n being Nat holds

( not n in X or not n in Y ) )

proof end;

:: deftheorem defines meets MEMBERED:def 24 :

for X, Y being natural-membered set holds

( not X meets Y iff for n being Nat holds

( not n in X or not n in Y ) );

for X, Y being natural-membered set holds

( not X meets Y iff for n being Nat holds

( not n in X or not n in Y ) );

theorem :: MEMBERED:25

for F being set st ( for X being set st X in F holds

X is complex-membered ) holds

union F is complex-membered

X is complex-membered ) holds

union F is complex-membered

proof end;

theorem :: MEMBERED:26

for F being set st ( for X being set st X in F holds

X is ext-real-membered ) holds

union F is ext-real-membered

X is ext-real-membered ) holds

union F is ext-real-membered

proof end;

theorem :: MEMBERED:27

for F being set st ( for X being set st X in F holds

X is real-membered ) holds

union F is real-membered

X is real-membered ) holds

union F is real-membered

proof end;

theorem :: MEMBERED:28

for F being set st ( for X being set st X in F holds

X is rational-membered ) holds

union F is rational-membered

X is rational-membered ) holds

union F is rational-membered

proof end;

theorem :: MEMBERED:29

for F being set st ( for X being set st X in F holds

X is integer-membered ) holds

union F is integer-membered

X is integer-membered ) holds

union F is integer-membered

proof end;

theorem :: MEMBERED:30

for F being set st ( for X being set st X in F holds

X is natural-membered ) holds

union F is natural-membered

X is natural-membered ) holds

union F is natural-membered

proof end;

theorem :: MEMBERED:31

for F, X being set st X in F & X is complex-membered holds

meet F is complex-membered by Th19, SETFAM_1:3;

meet F is complex-membered by Th19, SETFAM_1:3;

theorem :: MEMBERED:32

for F, X being set st X in F & X is ext-real-membered holds

meet F is ext-real-membered by Th20, SETFAM_1:3;

meet F is ext-real-membered by Th20, SETFAM_1:3;

theorem :: MEMBERED:33

for F, X being set st X in F & X is real-membered holds

meet F is real-membered by Th21, SETFAM_1:3;

meet F is real-membered by Th21, SETFAM_1:3;

theorem :: MEMBERED:34

for F, X being set st X in F & X is rational-membered holds

meet F is rational-membered by Th22, SETFAM_1:3;

meet F is rational-membered by Th22, SETFAM_1:3;

theorem :: MEMBERED:35

for F, X being set st X in F & X is integer-membered holds

meet F is integer-membered by Th23, SETFAM_1:3;

meet F is integer-membered by Th23, SETFAM_1:3;

theorem :: MEMBERED:36

for F, X being set st X in F & X is natural-membered holds

meet F is natural-membered by Th24, SETFAM_1:3;

meet F is natural-membered by Th24, SETFAM_1:3;

registration
end;

:: Added by AK, 2008.02.02

registration
end;

theorem :: MEMBERED:37

for X, Y being real-membered set st X <> {} & Y <> {} & ( for a, b being real number st a in X & b in Y holds

a <= b ) holds

ex d being real number st

( ( for a being real number st a in X holds

a <= d ) & ( for b being real number st b in Y holds

d <= b ) )

a <= b ) holds

ex d being real number st

( ( for a being real number st a in X holds

a <= d ) & ( for b being real number st b in Y holds

d <= b ) )

proof end;

:: Added, AK, 2010.04.23

definition

let X be set ;

end;
attr X is add-closed means :: MEMBERED:def 25

for x, y being complex number st x in X & y in X holds

x + y in X;

for x, y being complex number st x in X & y in X holds

x + y in X;

:: deftheorem defines add-closed MEMBERED:def 25 :

for X being set holds

( X is add-closed iff for x, y being complex number st x in X & y in X holds

x + y in X );

for X being set holds

( X is add-closed iff for x, y being complex number st x in X & y in X holds

x + y in X );

registration

coherence

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

b_{1} is add-closed

COMPLEX is add-closed

REAL is add-closed

RAT is add-closed

INT is add-closed

NAT is add-closed

ex b_{1} being set st

( not b_{1} is empty & b_{1} is add-closed & b_{1} is natural-membered )

end;
for b

b

proof end;

coherence COMPLEX is add-closed

proof end;

coherence REAL is add-closed

proof end;

coherence RAT is add-closed

proof end;

coherence INT is add-closed

proof end;

coherence NAT is add-closed

proof end;

existence ex b

( not b

proof end;