begin
theorem Th1:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (All a,A,G)),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th2:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
All (All ('not' a),A,G),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th3:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
All ('not' (Ex a,A,G)),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th4:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
All (Ex ('not' a),A,G),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem
canceled;
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (All ('not' a),A,G),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th7:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (Ex a,A,G)),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem
canceled;
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' 'not' (Ex (All a,B,G),A,G) by PARTIT_2:11, PARTIT_2:19;
theorem Th10:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) '<' 'not' (Ex (All a,B,G),A,G)
theorem Th11:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex a,B,G),A,G)
theorem
canceled;
theorem
canceled;
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (All a,A,G),B,G) '<' 'not' (All (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
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' 'not' (All (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
for
A,
B being
a_partition of
Y holds
'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (All 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
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (All a,A,G),B,G) '<' Ex ('not' (All a,B,G)),
A,
G
theorem Th18:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' Ex ('not' (All a,B,G)),
A,
G
theorem Th19:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
'not' (Ex (Ex a,A,G),B,G) '<' Ex ('not' (All a,B,G)),
A,
G
theorem Th20:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' All ('not' (All a,B,G)),
A,
G
theorem Th21:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) '<' All ('not' (All a,B,G)),
A,
G
theorem Th22:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
'not' (Ex (Ex a,A,G),B,G) '<' Ex ('not' (Ex a,B,G)),
A,
G
theorem Th23:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) = All ('not' (Ex a,B,G)),
A,
G
theorem Th24:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),
A,
G
theorem Th25:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
'not' (Ex (Ex a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),
A,
G
theorem Th26:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' All (Ex ('not' a),B,G),
A,
G
theorem Th27:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) '<' All (Ex ('not' a),B,G),
A,
G
theorem Th28:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
'not' (Ex (Ex a,A,G),B,G) '<' Ex (All ('not' a),B,G),
A,
G
theorem Th29:
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) = All (All ('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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (Ex a,A,G)),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y holds
All ('not' (Ex a,A,G)),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y holds
All ('not' (Ex a,A,G)),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (Ex a,A,G)),
B,
G = 'not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (Ex 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
for
A,
B being
a_partition of
Y holds
All ('not' (Ex 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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (Ex a,A,G)),
B,
G '<' All ('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
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (Ex a,A,G)),
B,
G '<' All ('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
for
A,
B being
a_partition of
Y holds
All ('not' (Ex a,A,G)),
B,
G '<' Ex ('not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (Ex a,A,G)),
B,
G = All ('not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (Ex 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
for
A,
B being
a_partition of
Y holds
All ('not' (Ex 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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex ('not' (Ex a,A,G)),
B,
G '<' All (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (Ex a,A,G)),
B,
G '<' All (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
for
A,
B being
a_partition of
Y holds
All ('not' (Ex a,A,G)),
B,
G '<' Ex (All ('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
for
A,
B being
a_partition of
Y st
G is
independent holds
All ('not' (Ex a,A,G)),
B,
G = All (All ('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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (All ('not' a),A,G),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All (All ('not' a),A,G),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y holds
All (All ('not' a),A,G),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All (All ('not' a),A,G),
B,
G '<' 'not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (Ex ('not' 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
for
A,
B being
a_partition of
Y st
G is
independent holds
All (Ex ('not' 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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (All ('not' 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
for
A,
B being
a_partition of
Y holds
All (All ('not' 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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (All ('not' a),A,G),
B,
G '<' All ('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
for
A,
B being
a_partition of
Y st
G is
independent holds
All (All ('not' a),A,G),
B,
G '<' All ('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
for
A,
B being
a_partition of
Y holds
All (All ('not' a),A,G),
B,
G '<' Ex ('not' (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
for
A,
B being
a_partition of
Y st
G is
independent holds
All (All ('not' a),A,G),
B,
G = All ('not' (Ex a,B,G)),
A,
G
theorem
canceled;
theorem
for
Y being non
empty set for
a being
Element of
Funcs Y,
BOOLEAN for
G being
Subset of
for
A,
B being
a_partition of
Y holds
All (Ex ('not' 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
for
A,
B being
a_partition of
Y st
G is
independent holds
Ex (All ('not' a),A,G),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G