begin
theorem Th1:
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th8:
theorem
canceled;
theorem
canceled;
theorem Th11:
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 Th15:
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 Th177:
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 Th211:
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 Th222:
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 Th233:
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)
theorem Th1:
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)
'<' '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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
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 (('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
(PARTITIONS Y) 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
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 ((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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
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' (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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
(PARTITIONS Y) 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
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 (('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
(PARTITIONS Y) 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)