begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
theorem
begin
theorem Th11:
theorem
canceled;
theorem Th13:
theorem
canceled;
theorem
begin
Lm1:
for Y being non empty set
for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
theorem Th16:
theorem Th17:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
All (All a,P,G),
Q,
G = All (All a,Q,G),
P,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
Ex (Ex a,P,G),
Q,
G = Ex (Ex a,Q,G),
P,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
Ex (All a,P,G),
Q,
G '<' All (Ex a,Q,G),
P,
G