:: BVFUNC11 semantic presentation

theorem Th1: :: BVFUNC11:1
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 st b3 '<' b4 holds
EqClass b2,b3 c= EqClass b2,b4
proof end;

theorem Th2: :: BVFUNC11:2
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 holds EqClass b2,b3 c= EqClass b2,(b3 '\/' b4)
proof end;

theorem Th3: :: BVFUNC11:3
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 holds EqClass b2,(b3 '/\' b4) c= EqClass b2,b3
proof end;

theorem Th4: :: BVFUNC11:4
for b1 being non empty set
for b2 being Element of b1
for b3 being a_partition of b1 holds
( EqClass b2,b3 c= EqClass b2,(%O b1) & EqClass b2,(%I b1) c= EqClass b2,b3 )
proof end;

theorem Th5: :: BVFUNC11:5
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 st b2 is independent & b2 = {b3,b4} & b3 <> b4 holds
for b5, b6 being set st b5 in b3 & b6 in b4 holds
b5 meets b6
proof end;

theorem Th6: :: BVFUNC11:6
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 st b2 is independent & b2 = {b3,b4} & b3 <> b4 holds
'/\' b2 = b3 '/\' b4
proof end;

theorem Th7: :: BVFUNC11:7
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 st b2 = {b3,b4} & b3 <> b4 holds
CompF b3,b2 = b4
proof end;

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

theorem Th9: :: BVFUNC11:9
canceled;

theorem Th10: :: BVFUNC11:10
canceled;

theorem Th11: :: BVFUNC11: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 st b3 is independent holds
All (All b2,b4,b3),b5,b3 '<' Ex (All b2,b5,b3),b4,b3
proof end;

theorem Th12: :: BVFUNC11:12
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 b2,b4,b3),b5,b3 '<' Ex (Ex b2,b5,b3),b4,b3
proof end;

theorem Th13: :: BVFUNC11:13
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 b2,b4,b3),b5,b3 '<' All (Ex b2,b5,b3),b4,b3
proof end;

theorem Th14: :: BVFUNC11: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 holds All (Ex b2,b4,b3),b5,b3 '<' Ex (Ex b2,b5,b3),b4,b3
proof end;

theorem Th15: :: BVFUNC11: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 holds 'not' (Ex (All b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th16: :: BVFUNC11: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 st b3 is independent holds
Ex ('not' (All b2,b4,b3)),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th17: :: BVFUNC11: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' (All (All b2,b4,b3),b5,b3) = Ex ('not' (All b2,b5,b3)),b4,b3
proof end;

theorem Th18: :: BVFUNC11: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
All ('not' (All b2,b4,b3)),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th19: :: BVFUNC11: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 st b3 is independent holds
'not' (All (All b2,b4,b3),b5,b3) = Ex (Ex ('not' b2),b5,b3),b4,b3
proof end;

theorem Th20: :: BVFUNC11: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 (All b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b4,b3),b5,b3
proof end;

theorem Th21: :: BVFUNC11: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 holds 'not' (All (Ex b2,b4,b3),b5,b3) = Ex (All ('not' b2),b4,b3),b5,b3
proof end;

theorem Th22: :: BVFUNC11: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 (All b2,b4,b3),b5,b3) = All (Ex ('not' b2),b4,b3),b5,b3
proof end;

theorem Th23: :: BVFUNC11: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 holds 'not' (All (All b2,b4,b3),b5,b3) = Ex (Ex ('not' b2),b4,b3),b5,b3
proof end;

theorem Th24: :: BVFUNC11: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
Ex (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b5,b3),b4,b3
proof end;

theorem Th25: :: BVFUNC11: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 All (All b2,b4,b3),b5,b3 '<' All (Ex b2,b4,b3),b5,b3
proof end;

theorem Th26: :: BVFUNC11: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 holds All (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b4,b3),b5,b3
proof end;

theorem Th27: :: BVFUNC11: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 holds Ex (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b4,b3),b5,b3
proof end;