:: BVFUNC13 semantic presentation 
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: BVFUNC13:1 
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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: :: BVFUNC13:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: BVFUNC13:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th9: :: BVFUNC13:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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)
theorem Th10: :: BVFUNC13:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: BVFUNC13:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: BVFUNC13:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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: :: BVFUNC13:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:40 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:41 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:42 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:43 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:44 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:45 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:46 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:47 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:48 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:49 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:50 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:51 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:52 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:53 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:54 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:55 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:56 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:57 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:58 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:59 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:60 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: BVFUNC13:61 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: BVFUNC13:62 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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