:: PBOOLE semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster empty-yielding set ;
existence
ex b1 being Function st b1 is empty-yielding
by RELAT_1:60;
end;

theorem :: PBOOLE:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function st f is non-empty holds
rng f is with_non-empty_elements
proof end;

theorem :: PBOOLE:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function holds
( f is empty-yielding iff ( f = {} or rng f = {{} } ) )
proof end;

definition
let I be set ;
canceled;
canceled;
mode ManySortedSet of I -> Function means :Def3: :: PBOOLE:def 3
dom it = I;
existence
ex b1 being Function st dom b1 = I
proof end;
end;

:: deftheorem PBOOLE:def 1 :
canceled;

:: deftheorem PBOOLE:def 2 :
canceled;

:: deftheorem Def3 defines ManySortedSet PBOOLE:def 3 :
for I being set
for b2 being Function holds
( b2 is ManySortedSet of I iff dom b2 = I );

scheme :: PBOOLE:sch 1
KuratowskiFunction{ F1() -> set , F2( set ) -> set } :
ex f being ManySortedSet of F1() st
for e being set st e in F1() holds
f . e in F2(e)
provided
A1: for e being set st e in F1() holds
F2(e) <> {}
proof end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
pred X in Y means :Def4: :: PBOOLE:def 4
for i being set st i in I holds
X . i in Y . i;
pred X c= Y means :Def5: :: PBOOLE:def 5
for i being set st i in I holds
X . i c= Y . i;
reflexivity
for X being ManySortedSet of I
for i being set st i in I holds
X . i c= X . i
;
end;

:: deftheorem Def4 defines in PBOOLE:def 4 :
for I being set
for X, Y being ManySortedSet of I holds
( X in Y iff for i being set st i in I holds
X . i in Y . i );

:: deftheorem Def5 defines c= PBOOLE:def 5 :
for I being set
for X, Y being ManySortedSet of I holds
( X c= Y iff for i being set st i in I holds
X . i c= Y . i );

definition
let I be non empty set ;
let X, Y be ManySortedSet of I;
:: original: in
redefine pred X in Y;
asymmetry
for X, Y being ManySortedSet of I st X in Y holds
not Y in X
proof end;
end;

scheme :: PBOOLE:sch 2
PSeparation{ F1() -> set , F2() -> ManySortedSet of F1(), P1[ set , set ] } :
ex X being ManySortedSet of F1() st
for i being set st i in F1() holds
for e being set holds
( e in X . i iff ( e in F2() . i & P1[i,e] ) )
proof end;

theorem Th3: :: PBOOLE:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i = Y . i ) holds
X = Y
proof end;

definition
let I be set ;
func [0] I -> ManySortedSet of I equals :: PBOOLE:def 6
I --> {} ;
coherence
I --> {} is ManySortedSet of I
proof end;
correctness
;
let X, Y be ManySortedSet of I;
func X \/ Y -> ManySortedSet of I means :Def7: :: PBOOLE:def 7
for i being set st i in I holds
it . i = (X . i) \/ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
proof end;
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) \/ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) \/ (X . i)
;
func X /\ Y -> ManySortedSet of I means :Def8: :: PBOOLE:def 8
for i being set st i in I holds
it . i = (X . i) /\ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
proof end;
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) /\ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) /\ (X . i)
;
func X \ Y -> ManySortedSet of I means :Def9: :: PBOOLE:def 9
for i being set st i in I holds
it . i = (X . i) \ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \ (Y . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
proof end;
pred X overlaps Y means :Def10: :: PBOOLE:def 10
for i being set st i in I holds
X . i meets Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i meets Y . i ) holds
for i being set st i in I holds
Y . i meets X . i
;
pred X misses Y means :Def11: :: PBOOLE:def 11
for i being set st i in I holds
X . i misses Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i misses Y . i ) holds
for i being set st i in I holds
Y . i misses X . i
;
end;

:: deftheorem defines [0] PBOOLE:def 6 :
for I being set holds [0] I = I --> {} ;

:: deftheorem Def7 defines \/ PBOOLE:def 7 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X \/ Y iff for i being set st i in I holds
b4 . i = (X . i) \/ (Y . i) );

:: deftheorem Def8 defines /\ PBOOLE:def 8 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X /\ Y iff for i being set st i in I holds
b4 . i = (X . i) /\ (Y . i) );

:: deftheorem Def9 defines \ PBOOLE:def 9 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X \ Y iff for i being set st i in I holds
b4 . i = (X . i) \ (Y . i) );

:: deftheorem Def10 defines overlaps PBOOLE:def 10 :
for I being set
for X, Y being ManySortedSet of I holds
( X overlaps Y iff for i being set st i in I holds
X . i meets Y . i );

:: deftheorem Def11 defines misses PBOOLE:def 11 :
for I being set
for X, Y being ManySortedSet of I holds
( X misses Y iff for i being set st i in I holds
X . i misses Y . i );

notation
let I be set ;
let X, Y be ManySortedSet of I;
antonym X does_not_overlap Y for X overlaps Y;
antonym X meets Y for X misses Y;
end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
func X \+\ Y -> ManySortedSet of I equals :: PBOOLE:def 12
(X \ Y) \/ (Y \ X);
correctness
coherence
(X \ Y) \/ (Y \ X) is ManySortedSet of I
;
;
commutativity
for b1, X, Y being ManySortedSet of I st b1 = (X \ Y) \/ (Y \ X) holds
b1 = (Y \ X) \/ (X \ Y)
;
end;

:: deftheorem defines \+\ PBOOLE:def 12 :
for I being set
for X, Y being ManySortedSet of I holds X \+\ Y = (X \ Y) \/ (Y \ X);

theorem Th4: :: PBOOLE:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I
for i being set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)
proof end;

theorem Th5: :: PBOOLE:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, I being set holds ([0] I) . i = {}
proof end;

theorem Th6: :: PBOOLE:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I st ( for i being set st i in I holds
X . i = {} ) holds
X = [0] I
proof end;

theorem Th7: :: PBOOLE:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X, Y being ManySortedSet of I st ( x in X or x in Y ) holds
x in X \/ Y
proof end;

theorem Th8: :: PBOOLE:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X, Y being ManySortedSet of I holds
( x in X /\ Y iff ( x in X & x in Y ) )
proof end;

theorem Th9: :: PBOOLE:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X, Y being ManySortedSet of I st x in X & X c= Y holds
x in Y
proof end;

theorem Th10: :: PBOOLE:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X overlaps Y
proof end;

theorem Th11: :: PBOOLE:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X overlaps Y holds
ex x being ManySortedSet of I st
( x in X & x in Y )
proof end;

theorem :: PBOOLE:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for x, X, Y being ManySortedSet of I st x in X \ Y holds
x in X
proof end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
:: original: =
redefine pred X = Y means :: PBOOLE:def 13
( X c= Y & Y c= X );
compatibility
( X = Y iff ( X c= Y & Y c= X ) )
proof end;
end;

:: deftheorem defines = PBOOLE:def 13 :
for I being set
for X, Y being ManySortedSet of I holds
( X = Y iff ( X c= Y & Y c= X ) );

theorem :: PBOOLE:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: PBOOLE:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & Y c= Z holds
X c= Z
proof end;

theorem Th16: :: PBOOLE:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X c= X \/ Y & Y c= X \/ Y )
proof end;

theorem Th17: :: PBOOLE:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X /\ Y c= X & X /\ Y c= Y )
proof end;

theorem Th18: :: PBOOLE:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Z, Y being ManySortedSet of I st X c= Z & Y c= Z holds
X \/ Y c= Z
proof end;

theorem Th19: :: PBOOLE:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Z, X, Y being ManySortedSet of I st Z c= X & Z c= Y holds
Z c= X /\ Y
proof end;

theorem :: PBOOLE:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
( X \/ Z c= Y \/ Z & Z \/ X c= Z \/ Y )
proof end;

theorem Th21: :: PBOOLE:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
( X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y )
proof end;

theorem Th22: :: PBOOLE:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \/ Z c= Y \/ V
proof end;

theorem :: PBOOLE:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X /\ Z c= Y /\ V
proof end;

theorem Th24: :: PBOOLE:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
( X \/ Y = Y & Y \/ X = Y )
proof end;

theorem Th25: :: PBOOLE:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
( X /\ Y = X & Y /\ X = X )
proof end;

theorem :: PBOOLE:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ Y c= X \/ Z
proof end;

theorem :: PBOOLE:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Z, Y being ManySortedSet of I st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z
proof end;

theorem :: PBOOLE:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y \/ Z iff ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) )
proof end;

theorem :: PBOOLE:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y /\ Z iff ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) )
proof end;

theorem :: PBOOLE:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: PBOOLE:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \/ Z = X \/ (Y \/ Z)
proof end;

theorem Th35: :: PBOOLE:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) /\ Z = X /\ (Y /\ Z)
proof end;

theorem Th36: :: PBOOLE:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X )
proof end;

theorem Th37: :: PBOOLE:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X )
proof end;

theorem Th38: :: PBOOLE:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
proof end;

theorem Th39: :: PBOOLE:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds
( X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z) & (Y /\ Z) \/ X = (Y \/ X) /\ (Z \/ X) )
proof end;

theorem :: PBOOLE:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st (X /\ Y) \/ (X /\ Z) = X holds
X c= Y \/ Z
proof end;

theorem :: PBOOLE:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st (X \/ Y) /\ (X \/ Z) = X holds
Y /\ Z c= X
proof end;

theorem :: PBOOLE:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
proof end;

theorem :: PBOOLE:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X \/ Y c= Z holds
( X c= Z & Y c= Z )
proof end;

theorem :: PBOOLE:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y /\ Z holds
( X c= Y & X c= Z )
proof end;

theorem :: PBOOLE:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds
( (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z) & X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z) )
proof end;

theorem :: PBOOLE:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds
( (X /\ Y) /\ Z = (X /\ Z) /\ (Y /\ Z) & X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z) )
proof end;

theorem :: PBOOLE:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X \/ (X \/ Y) = X \/ Y & (X \/ Y) \/ Y = X \/ Y )
proof end;

theorem :: PBOOLE:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X /\ (X /\ Y) = X /\ Y & (X /\ Y) /\ Y = X /\ Y )
proof end;

theorem Th49: :: PBOOLE:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds [0] I c= X
proof end;

theorem Th50: :: PBOOLE:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I st X c= [0] I holds
X = [0] I
proof end;

theorem Th51: :: PBOOLE:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y /\ Z = [0] I holds
X = [0] I
proof end;

theorem :: PBOOLE:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & Y /\ Z = [0] I holds
X /\ Z = [0] I
proof end;

theorem Th53: :: PBOOLE:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds
( X \/ ([0] I) = X & ([0] I) \/ X = X )
proof end;

theorem :: PBOOLE:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X \/ Y = [0] I holds
( X = [0] I & Y = [0] I )
proof end;

theorem :: PBOOLE:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds
( X /\ ([0] I) = [0] I & ([0] I) /\ X = [0] I )
proof end;

theorem :: PBOOLE:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y \/ Z & X /\ Z = [0] I holds
X c= Y
proof end;

theorem :: PBOOLE:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, X being ManySortedSet of I st Y c= X & X /\ Y = [0] I holds
Y = [0] I by Th25;

theorem Th58: :: PBOOLE:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X \ Y = [0] I iff X c= Y )
proof end;

theorem Th59: :: PBOOLE:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
X \ Z c= Y \ Z
proof end;

theorem Th60: :: PBOOLE:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
Z \ Y c= Z \ X
proof end;

theorem :: PBOOLE:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \ V c= Y \ Z
proof end;

theorem Th62: :: PBOOLE:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \ Y c= X
proof end;

theorem :: PBOOLE:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X c= Y \ X holds
X = [0] I
proof end;

theorem :: PBOOLE:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds X \ X = [0] I by Th58;

theorem Th65: :: PBOOLE:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds X \ ([0] I) = X
proof end;

theorem Th66: :: PBOOLE:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds ([0] I) \ X = [0] I
proof end;

theorem :: PBOOLE:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X \ (X \/ Y) = [0] I & X \ (Y \/ X) = [0] I )
proof end;

theorem Th68: :: PBOOLE:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ Z
proof end;

theorem Th69: :: PBOOLE:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( (X \ Y) /\ Y = [0] I & Y /\ (X \ Y) = [0] I )
proof end;

theorem Th70: :: PBOOLE:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
proof end;

theorem Th71: :: PBOOLE:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( (X \ Y) \/ (X /\ Y) = X & (X /\ Y) \/ (X \ Y) = X )
proof end;

theorem :: PBOOLE:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
( Y = X \/ (Y \ X) & Y = (Y \ X) \/ X )
proof end;

theorem Th73: :: PBOOLE:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X \/ (Y \ X) = X \/ Y & (Y \ X) \/ X = Y \/ X )
proof end;

theorem Th74: :: PBOOLE:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \ (X \ Y) = X /\ Y
proof end;

theorem Th75: :: PBOOLE:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proof end;

theorem Th76: :: PBOOLE:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X \ (X /\ Y) = X \ Y & X \ (Y /\ X) = X \ Y )
proof end;

theorem :: PBOOLE:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X /\ Y = [0] I iff X \ Y = X )
proof end;

theorem Th78: :: PBOOLE:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proof end;

theorem Th79: :: PBOOLE:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X \ Y) \ Z = X \ (Y \/ Z)
proof end;

theorem :: PBOOLE:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z)
proof end;

theorem Th81: :: PBOOLE:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ Y = X \ Y
proof end;

theorem :: PBOOLE:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y \/ Z holds
( X \ Y c= Z & X \ Z c= Y )
proof end;

theorem Th83: :: PBOOLE:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
proof end;

theorem Th84: :: PBOOLE:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) \ Y = X \ Y
proof end;

theorem :: PBOOLE:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proof end;

theorem :: PBOOLE:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X \ Y = Y \ X holds
X = Y
proof end;

theorem :: PBOOLE:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
proof end;

theorem :: PBOOLE:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X \ Y c= Z holds
X c= Y \/ Z
proof end;

theorem :: PBOOLE:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \ Y c= X \+\ Y by Th16;

theorem :: PBOOLE:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds
( X \+\ ([0] I) = X & ([0] I) \+\ X = X )
proof end;

theorem :: PBOOLE:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds X \+\ X = [0] I by Th58;

theorem :: PBOOLE:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \/ (X /\ Y)
proof end;

theorem Th95: :: PBOOLE:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \+\ Y = (X \/ Y) \ (X /\ Y)
proof end;

theorem :: PBOOLE:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
proof end;

theorem :: PBOOLE:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)
proof end;

theorem Th98: :: PBOOLE:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof end;

theorem :: PBOOLE:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X \ Y c= Z & Y \ X c= Z holds
X \+\ Y c= Z by Th18;

theorem Th100: :: PBOOLE:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \/ Y = X \+\ (Y \ X)
proof end;

theorem Th101: :: PBOOLE:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X /\ Y = X \+\ (X \ Y)
proof end;

theorem Th102: :: PBOOLE:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \ Y = X \+\ (X /\ Y)
proof end;

theorem Th103: :: PBOOLE:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, X being ManySortedSet of I holds Y \ X = X \+\ (X \/ Y)
proof end;

theorem :: PBOOLE:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)
proof end;

theorem :: PBOOLE:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
proof end;

theorem :: PBOOLE:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st ( X overlaps Y or X overlaps Z ) holds
X overlaps Y \/ Z
proof end;

theorem :: PBOOLE:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th108: :: PBOOLE:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y & Y c= Z holds
X overlaps Z
proof end;

theorem Th109: :: PBOOLE:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y & X c= Z holds
Z overlaps Y
proof end;

theorem Th110: :: PBOOLE:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V & X overlaps Z holds
Y overlaps V
proof end;

theorem :: PBOOLE:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y /\ Z holds
( X overlaps Y & X overlaps Z )
proof end;

theorem :: PBOOLE:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Z, V being ManySortedSet of I st X overlaps Z & X c= V holds
X overlaps Z /\ V
proof end;

theorem :: PBOOLE:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y \ Z holds
X overlaps Y
proof end;

theorem :: PBOOLE:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, Z, X being ManySortedSet of I st Y does_not_overlap Z holds
X /\ Y does_not_overlap X /\ Z
proof end;

theorem :: PBOOLE:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y \ Z holds
Y overlaps X \ Z
proof end;

theorem Th116: :: PBOOLE:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X meets Y & Y c= Z holds
X meets Z
proof end;

theorem :: PBOOLE:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th118: :: PBOOLE:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, X being ManySortedSet of I holds Y misses X \ Y
proof end;

theorem :: PBOOLE:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \ Y
proof end;

theorem :: PBOOLE:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \+\ Y
proof end;

theorem Th121: :: PBOOLE:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X /\ Y = [0] I
proof end;

theorem :: PBOOLE:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I st X <> [0] I holds
X meets X
proof end;

theorem :: PBOOLE:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y misses Z holds
X = [0] I
proof end;

theorem :: PBOOLE:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Z, V, X, Y being ManySortedSet of I st Z \/ V = X \/ Y & X misses Z & Y misses V holds
( X = V & Y = Z )
proof end;

theorem :: PBOOLE:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th126: :: PBOOLE:126  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X \ Y = X
proof end;

theorem :: PBOOLE:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
(X \/ Y) \ Y = X
proof end;

theorem :: PBOOLE:128  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X \ Y = X holds
X misses Y
proof end;

theorem :: PBOOLE:129  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds X \ Y misses Y \ X
proof end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
pred X [= Y means :Def14: :: PBOOLE:def 14
for x being ManySortedSet of I st x in X holds
x in Y;
reflexivity
for X, x being ManySortedSet of I st x in X holds
x in X
;
end;

:: deftheorem Def14 defines [= PBOOLE:def 14 :
for I being set
for X, Y being ManySortedSet of I holds
( X [= Y iff for x being ManySortedSet of I st x in X holds
x in Y );

theorem :: PBOOLE:130  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
X [= Y
proof end;

theorem :: PBOOLE:131  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PBOOLE:132  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X [= Y & Y [= Z holds
X [= Z
proof end;

theorem :: PBOOLE:133  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
[0] {} in [0] {}
proof end;

theorem :: PBOOLE:134  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ManySortedSet of {} holds X = {}
proof end;

theorem :: PBOOLE:135  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for X, Y being ManySortedSet of I st X overlaps Y holds
X meets Y
proof end;

theorem Th136: :: PBOOLE:136  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for x being ManySortedSet of I holds not x in [0] I
proof end;

theorem :: PBOOLE:137  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X /\ Y <> [0] I
proof end;

theorem :: PBOOLE:138  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for X being ManySortedSet of I holds
( X does_not_overlap [0] I & [0] I does_not_overlap X )
proof end;

theorem Th139: :: PBOOLE:139  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for X, Y being ManySortedSet of I st X /\ Y = [0] I holds
X does_not_overlap Y
proof end;

theorem :: PBOOLE:140  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for X being ManySortedSet of I st X overlaps X holds
X <> [0] I
proof end;

definition
let I be set ;
let X be ManySortedSet of I;
:: original: empty-yielding
redefine attr X is empty-yielding means :Def15: :: PBOOLE:def 15
for i being set st i in I holds
X . i is empty;
compatibility
( X is empty-yielding iff for i being set st i in I holds
X . i is empty )
proof end;
:: original: non-empty
redefine attr X is non-empty means :Def16: :: PBOOLE:def 16
for i being set st i in I holds
not X . i is empty;
compatibility
( X is non-empty iff for i being set st i in I holds
not X . i is empty )
proof end;
end;

:: deftheorem Def15 defines empty-yielding PBOOLE:def 15 :
for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff for i being set st i in I holds
X . i is empty );

:: deftheorem Def16 defines non-empty PBOOLE:def 16 :
for I being set
for X being ManySortedSet of I holds
( X is non-empty iff for i being set st i in I holds
not X . i is empty );

registration
let I be set ;
cluster V4 ManySortedSet of I;
existence
ex b1 being ManySortedSet of I st b1 is empty-yielding
proof end;
cluster V3 ManySortedSet of I;
existence
ex b1 being ManySortedSet of I st b1 is non-empty
proof end;
end;

registration
let I be non empty set ;
cluster V3 -> V4 ManySortedSet of I;
coherence
for b1 being ManySortedSet of I st b1 is non-empty holds
not b1 is empty-yielding
proof end;
cluster V4 -> V3 ManySortedSet of I;
coherence
for b1 being ManySortedSet of I st b1 is empty-yielding holds
not b1 is non-empty
proof end;
end;

theorem :: PBOOLE:141  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff X = [0] I )
proof end;

theorem :: PBOOLE:142  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, X being ManySortedSet of I st Y is empty-yielding & X c= Y holds
X is empty-yielding
proof end;

theorem Th143: :: PBOOLE:143  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X is non-empty & X c= Y holds
Y is non-empty
proof end;

theorem Th144: :: PBOOLE:144  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X is non-empty & X [= Y holds
X c= Y
proof end;

theorem :: PBOOLE:145  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I st X is non-empty & X [= Y holds
Y is non-empty
proof end;

theorem :: PBOOLE:146  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X being V3 ManySortedSet of I ex x being ManySortedSet of I st x in X
proof end;

theorem Th147: :: PBOOLE:147  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y being ManySortedSet of I
for X being V3 ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) holds
X = Y
proof end;

theorem :: PBOOLE:148  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, Z being ManySortedSet of I
for X being V3 ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) holds
X = Y /\ Z
proof end;

scheme :: PBOOLE:sch 3
MSSEx{ F1() -> set , P1[ set , set ] } :
ex f being ManySortedSet of F1() st
for i being set st i in F1() holds
P1[i,f . i]
provided
A1: for i being set st i in F1() holds
ex j being set st P1[i,j]
proof end;

scheme :: PBOOLE:sch 4
MSSLambda{ F1() -> set , F2( set ) -> set } :
ex f being ManySortedSet of F1() st
for i being set st i in F1() holds
f . i = F2(i)
proof end;

registration
let I be set ;
cluster Function-yielding ManySortedSet of I;
existence
ex b1 being ManySortedSet of I st b1 is Function-yielding
proof end;
end;

definition
let I be set ;
mode ManySortedFunction of I is Function-yielding ManySortedSet of I;
end;

theorem Th149: :: PBOOLE:149  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being V3 ManySortedSet of I holds not {} in rng M
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
mode Component of M is Element of rng M;
end;

theorem :: PBOOLE:150  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being ManySortedSet of I
for A being Component of M ex i being set st
( i in I & A = M . i )
proof end;

theorem :: PBOOLE:151  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for i being set st i in I holds
M . i is Component of M
proof end;

definition
let I be set ;
let B be ManySortedSet of I;
mode Element of B -> ManySortedSet of I means :: PBOOLE:def 17
for i being set st i in I holds
it . i is Element of B . i;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Element of B . i
proof end;
end;

:: deftheorem defines Element PBOOLE:def 17 :
for I being set
for B, b3 being ManySortedSet of I holds
( b3 is Element of B iff for i being set st i in I holds
b3 . i is Element of B . i );

definition
let I be set ;
let A, B be ManySortedSet of I;
mode ManySortedFunction of A,B -> ManySortedSet of I means :Def18: :: PBOOLE:def 18
for i being set st i in I holds
it . i is Function of A . i,B . i;
correctness
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Function of A . i,B . i
;
proof end;
end;

:: deftheorem Def18 defines ManySortedFunction PBOOLE:def 18 :
for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 is ManySortedFunction of A,B iff for i being set st i in I holds
b4 . i is Function of A . i,B . i );

registration
let I be set ;
let A, B be ManySortedSet of I;
cluster -> Function-yielding ManySortedFunction of A,B;
coherence
for b1 being ManySortedFunction of A,B holds b1 is Function-yielding
proof end;
end;

definition
let I be set ;
let M be ManySortedSet of I;
func M # -> ManySortedSet of I * means :Def19: :: PBOOLE:def 19
for i being Element of I * holds it . i = product (M * i);
existence
ex b1 being ManySortedSet of I * st
for i being Element of I * holds b1 . i = product (M * i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I * st ( for i being Element of I * holds b1 . i = product (M * i) ) & ( for i being Element of I * holds b2 . i = product (M * i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines # PBOOLE:def 19 :
for I being set
for M being ManySortedSet of I
for b3 being ManySortedSet of I * holds
( b3 = M # iff for i being Element of I * holds b3 . i = product (M * i) );

registration
let I be set ;
let M be V3 ManySortedSet of I;
cluster M # -> V3 V4 ;
coherence
M # is non-empty
proof end;
end;

definition
let I be set ;
let J be non empty set ;
let O be Function of I,J;
let F be ManySortedSet of J;
:: original: *
redefine func F * O -> ManySortedSet of I;
coherence
O * F is ManySortedSet of I
proof end;
end;

definition
let I be set ;
let J be non empty set ;
let O be Function of I,J;
let F be V3 ManySortedSet of J;
:: original: *
redefine func F * O -> V3 ManySortedSet of I;
coherence
O * F is V3 ManySortedSet of I
proof end;
end;

definition
let a be set ;
func *--> a -> Function of NAT ,{a} * means :Def20: :: PBOOLE:def 20
for n being Nat holds it . n = n |-> a;
existence
ex b1 being Function of NAT ,{a} * st
for n being Nat holds b1 . n = n |-> a
proof end;
uniqueness
for b1, b2 being Function of NAT ,{a} * st ( for n being Nat holds b1 . n = n |-> a ) & ( for n being Nat holds b2 . n = n |-> a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines *--> PBOOLE:def 20 :
for a being set
for b2 being Function of NAT ,{a} * holds
( b2 = *--> a iff for n being Nat holds b2 . n = n |-> a );

theorem Th152: :: PBOOLE:152  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for a, b being set holds ({a} --> b) * (n |-> a) = n |-> b
proof end;

theorem :: PBOOLE:153  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for n being Nat
for a being set
for M being ManySortedSet of {a} st M = {a} --> D holds
((M # ) * (*--> a)) . n = Funcs (Seg n),D
proof end;

definition
let I, i be set ;
:: original: -->
redefine func I --> i -> Function of I,{i};
coherence
I --> i is Function of I,{i}
proof end;
end;

scheme :: PBOOLE:sch 5
LambdaDMS{ F1() -> non empty set , F2( set ) -> set } :
ex X being ManySortedSet of F1() st
for d being Element of F1() holds X . d = F2(d)
proof end;

registration
let J be non empty set ;
let B be V3 ManySortedSet of J;
let j be Element of J;
cluster B . j -> non empty ;
coherence
not B . j is empty
by Def16;
end;

definition
let I be set ;
let X, Y be ManySortedSet of I;
func [|X,Y|] -> ManySortedSet of I means :: PBOOLE:def 21
for i being set st i in I holds
it . i = [:(X . i),(Y . i):];
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = [:(X . i),(Y . i):]
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = [:(X . i),(Y . i):] ) & ( for i being set st i in I holds
b2 . i = [:(X . i),(Y . i):] ) holds
b1 = b2
proof end;
end;

:: deftheorem defines [| PBOOLE:def 21 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = [|X,Y|] iff for i being set st i in I holds
b4 . i = [:(X . i),(Y . i):] );

definition
let I be set ;
let X, Y be ManySortedSet of I;
deffunc H1( set ) -> set = Funcs (X . $1),(Y . $1);
func MSFuncs X,Y -> ManySortedSet of I means :: PBOOLE:def 22
for i being set st i in I holds
it . i = Funcs (X . i),(Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = Funcs (X . i),(Y . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = Funcs (X . i),(Y . i) ) & ( for i being set st i in I holds
b2 . i = Funcs (X . i),(Y . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines MSFuncs PBOOLE:def 22 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = MSFuncs X,Y iff for i being set st i in I holds
b4 . i = Funcs (X . i),(Y . i) );

definition
let I be set ;
let M be ManySortedSet of I;
mode ManySortedSubset of M -> ManySortedSet of I means :Def23: :: PBOOLE:def 23
it c= M;
existence
ex b1 being ManySortedSet of I st b1 c= M
;
end;

:: deftheorem Def23 defines ManySortedSubset PBOOLE:def 23 :
for I being set
for M, b3 being ManySortedSet of I holds
( b3 is ManySortedSubset of M iff b3 c= M );

registration
let I be set ;
let M be V3 ManySortedSet of I;
cluster V3 ManySortedSubset of M;
existence
ex b1 being ManySortedSubset of M st b1 is non-empty
proof end;
end;

definition
let F, G be Function-yielding Function;
func G ** F -> Function-yielding Function means :: PBOOLE:def 24
( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds
it . i = (G . i) * (F . i) ) );
existence
ex b1 being Function-yielding Function st
( dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) )
proof end;
uniqueness
for b1, b2 being Function-yielding Function st dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) & dom b2 = (dom F) /\ (dom G) & ( for i being set st i in dom b2 holds
b2 . i = (G . i) * (F . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines ** PBOOLE:def 24 :
for F, G, b3 being Function-yielding Function holds
( b3 = G ** F iff ( dom b3 = (dom F) /\ (dom G) & ( for i being set st i in dom b3 holds
b3 . i = (G . i) * (F . i) ) ) );

definition
let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;
func F .:.: A -> ManySortedSet of I means :: PBOOLE:def 25
for i being set st i in I holds
it . i = (F . i) .: (A . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (F . i) .: (A . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (F . i) .: (A . i) ) & ( for i being set st i in I holds
b2 . i = (F . i) .: (A . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines .:.: PBOOLE:def 25 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F .:.: A iff for i being set st i in I holds
b4 . i = (F . i) .: (A . i) );

registration
let I be set ;
cluster [0] I -> V4 ;
coherence
[0] I is empty-yielding
proof end;
end;