:: BVFUNC_4 semantic presentation

theorem Th1: :: BVFUNC_4:1
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN st b2 '<' b3 'imp' b4 holds
b2 '&' b3 '<' b4
proof end;

theorem Th2: :: BVFUNC_4:2
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN st b2 '&' b3 '<' b4 holds
b2 '<' b3 'imp' b4
proof end;

theorem Th3: :: BVFUNC_4:3
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'or' (b2 '&' b3) = b2
proof end;

theorem Th4: :: BVFUNC_4:4
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 '&' (b2 'or' b3) = b2
proof end;

theorem Th5: :: BVFUNC_4:5
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 '&' ('not' b2) = O_el b1
proof end;

theorem Th6: :: BVFUNC_4:6
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 'or' ('not' b2) = I_el b1
proof end;

theorem Th7: :: BVFUNC_4:7
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'eqv' b3 = (b2 'imp' b3) '&' (b3 'imp' b2)
proof end;

theorem Th8: :: BVFUNC_4:8
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'imp' b3 = ('not' b2) 'or' b3
proof end;

theorem Th9: :: BVFUNC_4:9
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'xor' b3 = (('not' b2) '&' b3) 'or' (b2 '&' ('not' b3))
proof end;

theorem Th10: :: BVFUNC_4:10
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 'eqv' b3 = I_el b1 iff ( b2 'imp' b3 = I_el b1 & b3 'imp' b2 = I_el b1 ) )
proof end;

theorem Th11: :: BVFUNC_4:11
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN st b2 'eqv' b3 = I_el b1 & b3 'eqv' b4 = I_el b1 holds
b2 'eqv' b4 = I_el b1
proof end;

theorem Th12: :: BVFUNC_4:12
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN st b2 'eqv' b3 = I_el b1 holds
('not' b2) 'eqv' ('not' b3) = I_el b1
proof end;

theorem Th13: :: BVFUNC_4:13
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN st b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 holds
(b2 '&' b4) 'eqv' (b3 '&' b5) = I_el b1
proof end;

theorem Th14: :: BVFUNC_4:14
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN st b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 holds
(b2 'imp' b4) 'eqv' (b3 'imp' b5) = I_el b1
proof end;

theorem Th15: :: BVFUNC_4:15
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN st b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 holds
(b2 'or' b4) 'eqv' (b3 'or' b5) = I_el b1
proof end;

theorem Th16: :: BVFUNC_4:16
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN st b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 holds
(b2 'eqv' b4) 'eqv' (b3 'eqv' b5) = I_el b1
proof end;

theorem Th17: :: BVFUNC_4:17
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 holds All (b2 'eqv' b3),b5,b4 = (All (b2 'imp' b3),b5,b4) '&' (All (b3 'imp' b2),b5,b4)
proof end;

theorem Th18: :: BVFUNC_4: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 holds All b2,b4,b3 '<' Ex b2,b5,b3
proof end;

theorem Th19: :: BVFUNC_4:19
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 st b4 is independent & b5 in b4 & b3 is_independent_of b5,b4 & b2 'imp' b3 = I_el b1 holds
(All b2,b5,b4) 'imp' b3 = I_el b1
proof end;

theorem Th20: :: BVFUNC_4:20
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4 being a_partition of b1 st b2 is_independent_of b4,b3 holds
Ex b2,b4,b3 '<' b2
proof end;

theorem Th21: :: BVFUNC_4:21
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4 being a_partition of b1 st b2 is_independent_of b4,b3 holds
b2 '<' All b2,b4,b3
proof end;

theorem Th22: :: BVFUNC_4: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 st b2 is_independent_of b5,b3 holds
All b2,b4,b3 '<' All b2,b5,b3
proof end;

theorem Th23: :: BVFUNC_4: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 b2 is_independent_of b4,b3 holds
Ex b2,b4,b3 '<' Ex b2,b5,b3
proof end;

theorem Th24: :: BVFUNC_4:24
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 holds All (b2 'eqv' b3),b5,b4 '<' (All b2,b5,b4) 'eqv' (All b3,b5,b4)
proof end;

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

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

theorem Th27: :: BVFUNC_4:27
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 st b2 'eqv' b3 = I_el b1 holds
(All b2,b5,b4) 'eqv' (All b3,b5,b4) = I_el b1
proof end;

theorem Th28: :: BVFUNC_4:28
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 st b2 'eqv' b3 = I_el b1 holds
(Ex b2,b5,b4) 'eqv' (Ex b3,b5,b4) = I_el b1
proof end;