:: by Andrzej Trybulec

::

:: Received August 23, 2003

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

definition

let X be set ;

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

for x being object st x in X holds

x is complex ;

for x being object st x in X holds

x is complex ;

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

for x being object st x in X holds

x is ext-real ;

for x being object st x in X holds

x is ext-real ;

attr X is real-membered means :Def3: :: MEMBERED:def 3

for x being object st x in X holds

x is real ;

for x being object st x in X holds

x is real ;

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

for x being object st x in X holds

x is rational ;

for x being object st x in X holds

x is rational ;

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

for x being object st x in X holds

x is integer ;

for x being object st x in X holds

x is integer ;

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

for x being object st x in X holds

x is natural ;

for x being object 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 object st x in X holds

x is complex );

for X being set holds

( X is complex-membered iff for x being object 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 object st x in X holds

x is ext-real );

for X being set holds

( X is ext-real-membered iff for x being object 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 object st x in X holds

x is real );

for X being set holds

( X is real-membered iff for x being object 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 object st x in X holds

x is rational );

for X being set holds

( X is rational-membered iff for x being object 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 object st x in X holds

x is integer );

for X being set holds

( X is integer-membered iff for x being object 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 object st x in X holds

x is natural );

for X being set holds

( X is natural-membered iff for x being object 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

COMPLEX is complex-membered ;

coherence

ExtREAL is ext-real-membered

REAL is real-membered ;

coherence

RAT is rational-membered

INT is integer-membered ;

coherence

NAT is natural-membered ;

end;
COMPLEX is complex-membered ;

coherence

ExtREAL is ext-real-membered

proof end;

coherence REAL is real-membered ;

coherence

RAT is rational-membered

proof end;

coherence INT is integer-membered ;

coherence

NAT is natural-membered ;

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

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

registration
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

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

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

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 ;

compatibility

( X c= Y iff for c being Complex st c in X holds

c in Y ) ;

end;
let Y be set ;

compatibility

( X c= Y iff for c being Complex st c in X holds

c in Y ) ;

:: deftheorem defines c= MEMBERED:def 7 :

for X being complex-membered set

for Y being set holds

( X c= Y iff for c being Complex 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 st c in X holds

c in Y );

definition

let X be ext-real-membered set ;

let Y be set ;

compatibility

( X c= Y iff for e being ExtReal st e in X holds

e in Y ) ;

end;
let Y be set ;

compatibility

( X c= Y iff for e being ExtReal st e in X holds

e in Y ) ;

:: deftheorem defines c= MEMBERED:def 8 :

for X being ext-real-membered set

for Y being set holds

( X c= Y iff for e being ExtReal 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 ExtReal 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 st r in X holds

r in Y ) ;

end;
let Y be set ;

compatibility

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

r in Y ) ;

:: deftheorem defines c= MEMBERED:def 9 :

for X being real-membered set

for Y being set holds

( X c= Y iff for r being Real 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 st r in X holds

r in Y );

definition

let X be rational-membered set ;

let Y be set ;

compatibility

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

w in Y ) ;

end;
let Y be set ;

compatibility

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

w in Y ) ;

:: deftheorem defines c= MEMBERED:def 10 :

for X being rational-membered set

for Y being set holds

( X c= Y iff for w being Rational 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 st w in X holds

w in Y );

definition

let X be integer-membered set ;

let Y be set ;

compatibility

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

i in Y ) ;

end;
let Y be set ;

compatibility

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

i in Y ) ;

:: deftheorem defines c= MEMBERED:def 11 :

for X being integer-membered set

for Y being set holds

( X c= Y iff for i being Integer 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 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 ) ;

:: deftheorem 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 ;

compatibility

( X = Y iff for c being Complex holds

( c in X iff c in Y ) )

end;
compatibility

( X = Y iff for c being Complex 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 holds

( c in X iff c in Y ) );

for X, Y being complex-membered set holds

( X = Y iff for c being Complex holds

( c in X iff c in Y ) );

definition

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

compatibility

( X = Y iff for e being ExtReal holds

( e in X iff e in Y ) )

end;
compatibility

( X = Y iff for e being ExtReal 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 ExtReal holds

( e in X iff e in Y ) );

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

( X = Y iff for e being ExtReal holds

( e in X iff e in Y ) );

definition

let X, Y be real-membered set ;

compatibility

( X = Y iff for r being Real holds

( r in X iff r in Y ) ) ;

end;
compatibility

( X = Y iff for r being Real holds

( r in X iff r in Y ) ) ;

:: deftheorem defines = MEMBERED:def 15 :

for X, Y being real-membered set holds

( X = Y iff for r being Real holds

( r in X iff r in Y ) );

for X, Y being real-membered set holds

( X = Y iff for r being Real holds

( r in X iff r in Y ) );

definition

let X, Y be rational-membered set ;

compatibility

( X = Y iff for w being Rational holds

( w in X iff w in Y ) ) ;

end;
compatibility

( X = Y iff for w being Rational holds

( w in X iff w in Y ) ) ;

:: deftheorem defines = MEMBERED:def 16 :

for X, Y being rational-membered set holds

( X = Y iff for w being Rational holds

( w in X iff w in Y ) );

for X, Y being rational-membered set holds

( X = Y iff for w being Rational holds

( w in X iff w in Y ) );

definition

let X, Y be integer-membered set ;

compatibility

( X = Y iff for i being Integer holds

( i in X iff i in Y ) ) ;

end;
compatibility

( X = Y iff for i being Integer holds

( i in X iff i in Y ) ) ;

:: deftheorem defines = MEMBERED:def 17 :

for X, Y being integer-membered set holds

( X = Y iff for i being Integer holds

( i in X iff i in Y ) );

for X, Y being integer-membered set holds

( X = Y iff for i being Integer 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 ) ) ;

:: 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 holds

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

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

for c being Complex holds

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

compatibility for c being Complex holds

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

( not X meets Y iff for c being Complex 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 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 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 ExtReal holds

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

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

for e being ExtReal holds

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

compatibility for e being ExtReal holds

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

( not X meets Y iff for e being ExtReal 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 ExtReal 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 ExtReal 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 holds

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

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

for r being Real holds

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

compatibility for r being Real holds

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

( not X meets Y iff for r being Real holds

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

:: deftheorem defines meets MEMBERED:def 21 :

for X, Y being real-membered set holds

( not X meets Y iff for r being Real 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 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 holds

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

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

for w being Rational holds

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

compatibility for w being Rational holds

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

( not X meets Y iff for w being Rational holds

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

:: deftheorem defines meets MEMBERED:def 22 :

for X, Y being rational-membered set holds

( not X meets Y iff for w being Rational 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 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 holds

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

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

for i being Integer holds

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

compatibility for i being Integer holds

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

( not X meets Y iff for i being Integer holds

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

:: deftheorem defines meets MEMBERED:def 23 :

for X, Y being integer-membered set holds

( not X meets Y iff for i being Integer 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 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 ) ) ;

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

theorem :: MEMBERED:37

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

a <= b ) holds

ex d being Real st

( ( for a being Real st a in X holds

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

d <= b ) )

a <= b ) holds

ex d being Real st

( ( for a being Real st a in X holds

a <= d ) & ( for b being Real 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 st x in X & y in X holds

x + y in X;

for x, y being Complex 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 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 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
;

coherence

COMPLEX is add-closed by XCMPLX_0:def 2;

coherence

REAL is add-closed by XREAL_0:def 1;

coherence

RAT is add-closed by RAT_1:def 2;

coherence

INT is add-closed by INT_1:def 2;

coherence

NAT is add-closed by ORDINAL1:def 12;

existence

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

coherence

COMPLEX is add-closed by XCMPLX_0:def 2;

coherence

REAL is add-closed by XREAL_0:def 1;

coherence

RAT is add-closed by RAT_1:def 2;

coherence

INT is add-closed by INT_1:def 2;

coherence

NAT is add-closed by ORDINAL1:def 12;

existence

ex b

( not b

proof end;