:: BVFUNC13 semantic presentation

theorem Th1: :: BVFUNC13:1
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (All b2,b4,b3)),b5,b3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th2: :: BVFUNC13:2
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All (All ('not' b2),b4,b3),b5,b3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th3: :: BVFUNC13:3
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th4: :: BVFUNC13:4
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (Ex ('not' b2),b4,b3),b5,b3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th5: :: BVFUNC13:5
canceled;

theorem Th6: :: BVFUNC13:6
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (All ('not' b2),b4,b3),b5,b3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th7: :: BVFUNC13:7
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (Ex b2,b4,b3)),b5,b3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th8: :: BVFUNC13:8
canceled;

theorem Th9: :: BVFUNC13:9
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (All (Ex b2,b4,b3),b5,b3) '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof end;

theorem Th10: :: BVFUNC13:10
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof end;

theorem Th11: :: BVFUNC13:11
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds 'not' (Ex (Ex b2,b4,b3),b5,b3) '<' 'not' (All (Ex b2,b5,b3),b4,b3)
proof end;

theorem Th12: :: BVFUNC13:12
canceled;

theorem Th13: :: BVFUNC13:13
canceled;

theorem Th14: :: BVFUNC13:14
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (All b2,b4,b3),b5,b3) '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th15: :: BVFUNC13:15
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (All (Ex b2,b4,b3),b5,b3) '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th16: :: BVFUNC13:16
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds 'not' (Ex (Ex b2,b4,b3),b5,b3) '<' 'not' (All (All b2,b5,b3),b4,b3)
proof end;

theorem Th17: :: BVFUNC13:17
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (All b2,b4,b3),b5,b3) '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th18: :: BVFUNC13:18
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (All (Ex b2,b4,b3),b5,b3) '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th19: :: BVFUNC13:19
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds 'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th20: :: BVFUNC13:20
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (All (Ex b2,b4,b3),b5,b3) '<' All ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th21: :: BVFUNC13:21
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' All ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th22: :: BVFUNC13:22
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds 'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex ('not' (Ex b2,b5,b3)),b4,b3
proof end;

theorem Th23: :: BVFUNC13:23
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (Ex b2,b4,b3),b5,b3) = All ('not' (Ex b2,b5,b3)),b4,b3
proof end;

theorem Th24: :: BVFUNC13:24
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (All (Ex b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th25: :: BVFUNC13:25
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds 'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th26: :: BVFUNC13:26
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (All (Ex b2,b4,b3),b5,b3) '<' All (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th27: :: BVFUNC13:27
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' All (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th28: :: BVFUNC13:28
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds 'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex (All ('not' b2),b5,b3),b4,b3
proof end;

theorem Th29: :: BVFUNC13:29
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
'not' (Ex (Ex b2,b4,b3),b5,b3) = All (All ('not' b2),b5,b3),b4,b3
proof end;

theorem Th30: :: BVFUNC13:30
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (Ex b2,b4,b3)),b5,b3 '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof end;

theorem Th31: :: BVFUNC13:31
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof end;

theorem Th32: :: BVFUNC13:32
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' 'not' (All (Ex b2,b5,b3),b4,b3)
proof end;

theorem Th33: :: BVFUNC13:33
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (Ex b2,b4,b3)),b5,b3 = 'not' (Ex (Ex b2,b5,b3),b4,b3)
proof end;

theorem Th34: :: BVFUNC13:34
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (All b2,b4,b3)),b5,b3 = Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th35: :: BVFUNC13:35
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (All b2,b4,b3)),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th36: :: BVFUNC13:36
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (Ex b2,b4,b3)),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th37: :: BVFUNC13:37
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th38: :: BVFUNC13:38
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (Ex b2,b4,b3)),b5,b3 '<' All ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th39: :: BVFUNC13:39
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (Ex b2,b4,b3)),b5,b3 '<' All ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th40: :: BVFUNC13:40
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' Ex ('not' (Ex b2,b5,b3)),b4,b3
proof end;

theorem Th41: :: BVFUNC13:41
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (Ex b2,b4,b3)),b5,b3 = All ('not' (Ex b2,b5,b3)),b4,b3
proof end;

theorem Th42: :: BVFUNC13:42
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (Ex b2,b4,b3)),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th43: :: BVFUNC13:43
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th44: :: BVFUNC13:44
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex ('not' (Ex b2,b4,b3)),b5,b3 '<' All (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th45: :: BVFUNC13:45
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (Ex b2,b4,b3)),b5,b3 '<' All (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th46: :: BVFUNC13:46
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All ('not' (Ex b2,b4,b3)),b5,b3 '<' Ex (All ('not' b2),b5,b3),b4,b3
proof end;

theorem Th47: :: BVFUNC13:47
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All ('not' (Ex b2,b4,b3)),b5,b3 = All (All ('not' b2),b5,b3),b4,b3
proof end;

theorem Th48: :: BVFUNC13:48
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (All ('not' b2),b4,b3),b5,b3 '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof end;

theorem Th49: :: BVFUNC13:49
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (All ('not' b2),b4,b3),b5,b3 '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof end;

theorem Th50: :: BVFUNC13:50
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All (All ('not' b2),b4,b3),b5,b3 '<' 'not' (All (Ex b2,b5,b3),b4,b3)
proof end;

theorem Th51: :: BVFUNC13:51
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (All ('not' b2),b4,b3),b5,b3 '<' 'not' (Ex (Ex b2,b5,b3),b4,b3)
proof end;

theorem Th52: :: BVFUNC13:52
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (Ex ('not' b2),b4,b3),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th53: :: BVFUNC13:53
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (Ex ('not' b2),b4,b3),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th54: :: BVFUNC13:54
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (All ('not' b2),b4,b3),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th55: :: BVFUNC13:55
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All (All ('not' b2),b4,b3),b5,b3 '<' Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th56: :: BVFUNC13:56
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (All ('not' b2),b4,b3),b5,b3 '<' All ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th57: :: BVFUNC13:57
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (All ('not' b2),b4,b3),b5,b3 '<' All ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th58: :: BVFUNC13:58
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All (All ('not' b2),b4,b3),b5,b3 '<' Ex ('not' (Ex b2,b5,b3)),b4,b3
proof end;

theorem Th59: :: BVFUNC13:59
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (All ('not' b2),b4,b3),b5,b3 = All ('not' (Ex b2,b5,b3)),b4,b3
proof end;

theorem Th60: :: BVFUNC13:60
canceled;

theorem Th61: :: BVFUNC13:61
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All (Ex ('not' b2),b4,b3),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th62: :: BVFUNC13:62
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (All ('not' b2),b4,b3),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;