:: BVFUNC_3 semantic presentation

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

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

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

theorem Th4: :: BVFUNC_3:4
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds 'not' ((All b3,b5,b2) '&' (All b4,b5,b2)) = (Ex ('not' b3),b5,b2) 'or' (Ex ('not' b4),b5,b2)
proof end;

theorem Th5: :: BVFUNC_3:5
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds 'not' ((Ex b3,b5,b2) '&' (Ex b4,b5,b2)) = (All ('not' b3),b5,b2) 'or' (All ('not' b4),b5,b2)
proof end;

theorem Th6: :: BVFUNC_3:6
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds (All b3,b5,b2) 'or' (All b4,b5,b2) '<' b3 'or' b4
proof end;

theorem Th7: :: BVFUNC_3:7
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds b3 'or' b4 '<' (Ex b3,b5,b2) 'or' (Ex b4,b5,b2)
proof end;

theorem Th8: :: BVFUNC_3:8
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds b3 'xor' b4 '<' ('not' ((Ex ('not' b3),b5,b2) 'xor' (Ex b4,b5,b2))) 'or' ('not' ((Ex b3,b5,b2) 'xor' (Ex ('not' b4),b5,b2)))
proof end;

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

E1: now
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Subset of (PARTITIONS c1);
let c5 be a_partition of c1;
let c6 be Element of c1;
assume E2: Pj (All (c2 'or' c3),c5,c4),c6 = TRUE ;
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c4) & not Pj (c2 'or' c3),b1 = TRUE ) ;
then Pj (B_INF (c2 'or' c3),(CompF c5,c4)),c6 = FALSE by BVFUNC_1:def 19;
then Pj (All (c2 'or' c3),c5,c4),c6 = FALSE by BVFUNC_2:def 9;
hence contradiction by E2, MARGREL1:43;
end;

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

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

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

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

E2: now
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Subset of (PARTITIONS c1);
let c5 be a_partition of c1;
let c6 be Element of c1;
assume E3: Pj (All (c2 'imp' c3),c5,c4),c6 = TRUE ;
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c4) & not Pj (c2 'imp' c3),b1 = TRUE ) ;
then Pj (B_INF (c2 'imp' c3),(CompF c5,c4)),c6 = FALSE by BVFUNC_1:def 19;
then Pj (All (c2 'imp' c3),c5,c4),c6 = FALSE by BVFUNC_2:def 9;
hence contradiction by E3, MARGREL1:43;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th27: :: BVFUNC_3:27
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds All (b3 'imp' b4),b5,b2 = 'not' (Ex (b3 '&' ('not' b4)),b5,b2)
proof end;

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

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

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

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

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

theorem Th33: :: BVFUNC_3:33
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being Element of Funcs b1,BOOLEAN
for b6 being a_partition of b1 holds (All (b3 'imp' b4),b6,b2) '&' (Ex (b5 '&' b3),b6,b2) '<' Ex (b5 '&' b4),b6,b2
proof end;

theorem Th34: :: BVFUNC_3:34
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being Element of Funcs b1,BOOLEAN
for b6 being a_partition of b1 holds (All (b3 'imp' ('not' b4)),b6,b2) '&' (All (b5 'imp' b4),b6,b2) '<' All (b5 'imp' ('not' b3)),b6,b2
proof end;

theorem Th35: :: BVFUNC_3:35
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being Element of Funcs b1,BOOLEAN
for b6 being a_partition of b1 holds (All (b3 'imp' b4),b6,b2) '&' (All (b5 'imp' ('not' b4)),b6,b2) '<' All (b5 'imp' ('not' b3)),b6,b2
proof end;

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

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

theorem Th38: :: BVFUNC_3:38
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being Element of Funcs b1,BOOLEAN
for b6 being a_partition of b1 holds ((Ex b3,b6,b2) '&' (All (b3 'imp' b4),b6,b2)) '&' (All (b3 'imp' b5),b6,b2) '<' Ex (b5 '&' b4),b6,b2
proof end;

theorem Th39: :: BVFUNC_3:39
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being Element of Funcs b1,BOOLEAN
for b6 being a_partition of b1 holds (All (b3 'imp' b4),b6,b2) '&' (All (b4 'imp' ('not' b5)),b6,b2) '<' All (b5 'imp' ('not' b3)),b6,b2
proof end;

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

theorem Th41: :: BVFUNC_3:41
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being Element of Funcs b1,BOOLEAN
for b6 being a_partition of b1 holds ((Ex b3,b6,b2) '&' (All (b4 'imp' ('not' b3)),b6,b2)) '&' (All (b3 'imp' b5),b6,b2) '<' Ex (b5 '&' ('not' b4)),b6,b2
proof end;