:: by Library Committee

::

:: Received April 6, 2002

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

begin

definition
end;

:: deftheorem Def1 defines empty XBOOLE_0:def 1 :

for X being set holds

( X is empty iff for x being set holds not x in X );

for X being set holds

( X is empty iff for x being set holds not x in X );

definition

coherence

the empty set is set ;

let X, Y be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X or x in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X or x in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X or x in Y ) ) ) holds

b_{1} = b_{2}

for b_{1}, X, Y being set st ( for x being set holds

( x in b_{1} iff ( x in X or x in Y ) ) ) holds

for x being set holds

( x in b_{1} iff ( x in Y or x in X ) )
;

idempotence

for X, x being set holds

( x in X iff ( x in X or x in X ) ) ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X & x in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X & x in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & x in Y ) ) ) holds

b_{1} = b_{2}

for b_{1}, X, Y being set st ( for x being set holds

( x in b_{1} iff ( x in X & x in Y ) ) ) holds

for x being set holds

( x in b_{1} iff ( x in Y & x in X ) )
;

idempotence

for X, x being set holds

( x in X iff ( x in X & x in X ) ) ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X & not x in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X & not x in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & not x in Y ) ) ) holds

b_{1} = b_{2}

end;
the empty set is set ;

let X, Y be set ;

func X \/ Y -> set means :Def3: :: XBOOLE_0:def 3

for x being set holds

( x in it iff ( x in X or x in Y ) );

existence for x being set holds

( x in it iff ( x in X or x in Y ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

commutativity for b

( x in b

for x being set holds

( x in b

idempotence

for X, x being set holds

( x in X iff ( x in X or x in X ) ) ;

func X /\ Y -> set means :Def4: :: XBOOLE_0:def 4

for x being set holds

( x in it iff ( x in X & x in Y ) );

existence for x being set holds

( x in it iff ( x in X & x in Y ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

commutativity for b

( x in b

for x being set holds

( x in b

idempotence

for X, x being set holds

( x in X iff ( x in X & x in X ) ) ;

func X \ Y -> set means :Def5: :: XBOOLE_0:def 5

for x being set holds

( x in it iff ( x in X & not x in Y ) );

existence for x being set holds

( x in it iff ( x in X & not x in Y ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines \/ XBOOLE_0:def 3 :

for X, Y, b_{3} being set holds

( b_{3} = X \/ Y iff for x being set holds

( x in b_{3} iff ( x in X or x in Y ) ) );

for X, Y, b

( b

( x in b

:: deftheorem Def4 defines /\ XBOOLE_0:def 4 :

for X, Y, b_{3} being set holds

( b_{3} = X /\ Y iff for x being set holds

( x in b_{3} iff ( x in X & x in Y ) ) );

for X, Y, b

( b

( x in b

:: deftheorem Def5 defines \ XBOOLE_0:def 5 :

for X, Y, b_{3} being set holds

( b_{3} = X \ Y iff for x being set holds

( x in b_{3} iff ( x in X & not x in Y ) ) );

for X, Y, b

( b

( x in b

definition

let X, Y be set ;

correctness

coherence

(X \ Y) \/ (Y \ X) is set ;

;

commutativity

for b_{1}, X, Y being set st b_{1} = (X \ Y) \/ (Y \ X) holds

b_{1} = (Y \ X) \/ (X \ Y)
;

symmetry

for X, Y being set st X /\ Y = {} holds

Y /\ X = {} ;

irreflexivity

for X being set holds

( not X c= X or not X <> X ) ;

asymmetry

for X, Y being set st X c= Y & X <> Y & Y c= X holds

not Y <> X

for X being set holds

( X c= X or X c= X ) ;

symmetry

for X, Y being set holds

( ( not X c= Y & not Y c= X ) or Y c= X or X c= Y ) ;

compatibility

( X = Y iff ( X c= Y & Y c= X ) )

end;
correctness

coherence

(X \ Y) \/ (Y \ X) is set ;

;

commutativity

for b

b

symmetry

for X, Y being set st X /\ Y = {} holds

Y /\ X = {} ;

irreflexivity

for X being set holds

( not X c= X or not X <> X ) ;

asymmetry

for X, Y being set st X c= Y & X <> Y & Y c= X holds

not Y <> X

proof end;

reflexivity for X being set holds

( X c= X or X c= X ) ;

symmetry

for X, Y being set holds

( ( not X c= Y & not Y c= X ) or Y c= X or X c= Y ) ;

compatibility

( X = Y iff ( X c= Y & Y c= X ) )

proof end;

:: deftheorem Def7 defines misses XBOOLE_0:def 7 :

for X, Y being set holds

( X misses Y iff X /\ Y = {} );

for X, Y being set holds

( X misses Y iff X /\ Y = {} );

:: deftheorem Def8 defines c< XBOOLE_0:def 8 :

for X, Y being set holds

( X c< Y iff ( X c= Y & X <> Y ) );

for X, Y being set holds

( X c< Y iff ( X c= Y & X <> Y ) );

:: deftheorem defines are_c=-comparable XBOOLE_0:def 9 :

for X, Y being set holds

( X,Y are_c=-comparable iff ( X c= Y or Y c= X ) );

for X, Y being set holds

( X,Y are_c=-comparable iff ( X c= Y or Y c= X ) );

:: deftheorem defines = XBOOLE_0:def 10 :

for X, Y being set holds

( X = Y iff ( X c= Y & Y c= X ) );

for X, Y being set holds

( X = Y iff ( X c= Y & Y c= X ) );

theorem :: XBOOLE_0:1

for x, X, Y being set holds

( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )

( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )

proof end;

theorem :: XBOOLE_0:2

for X, Y, Z being set st ( for x being set holds

( not x in X iff ( x in Y iff x in Z ) ) ) holds

X = Y \+\ Z

( not x in X iff ( x in Y iff x in Z ) ) ) holds

X = Y \+\ Z

proof end;

registration

let x1 be set ;

coherence

not {x1} is empty

coherence

not {x1,x2} is empty

end;
coherence

not {x1} is empty

proof end;

let x2 be set ;coherence

not {x1,x2} is empty

proof end;

registration
end;

registration

let D be non empty set ;

let X be set ;

coherence

not D \/ X is empty

not X \/ D is empty ;

end;
let X be set ;

coherence

not D \/ X is empty

proof end;

coherence not X \/ D is empty ;

Lm1: for X being set st X is empty holds

X = {}

proof end;

theorem :: XBOOLE_0:5

begin

:: from RLSUB_2, 2006.12.02, AT

:: 2008.08.07, A.T.