begin
theorem Th1:
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th8:
theorem
canceled;
theorem
canceled;
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
All (All a,A,G),
B,
G '<' Ex (All a,B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
All (All a,A,G),
B,
G '<' Ex (Ex a,B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
All (All a,A,G),
B,
G '<' All (Ex a,B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
All (Ex a,A,G),
B,
G '<' Ex (Ex a,B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
'not' (Ex (All a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),
A,
G
theorem Th16:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (All a,A,G)),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G
theorem Th17:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (All a,A,G),B,G) = Ex ('not' (All a,B,G)),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (All a,A,G)),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (All a,A,G),B,G) = Ex (Ex ('not' a),B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (All a,A,G),B,G) '<' Ex (Ex ('not' a),A,G),
B,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
'not' (All (Ex a,A,G),B,G) = Ex (All ('not' a),A,G),
B,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
'not' (Ex (All a,A,G),B,G) = All (Ex ('not' a),A,G),
B,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
'not' (All (All a,A,G),B,G) = Ex (Ex ('not' a),A,G),
B,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (All a,A,G),
B,
G '<' Ex (Ex a,B,G),
A,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
All (All a,A,G),
B,
G '<' All (Ex a,A,G),
B,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
All (All a,A,G),
B,
G '<' Ex (Ex a,A,G),
B,
G
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
A,
B being
a_partition of
Y holds
Ex (All a,A,G),
B,
G '<' Ex (Ex a,A,G),
B,
G