:: Predicate Calculus for Boolean Valued Functions, III
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received July 14, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: BVFUNC11:1
for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y st PA '<' PB holds
EqClass (z,PA) c= EqClass (z,PB)
proofend;

theorem :: BVFUNC11:2
for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,PA) c= EqClass (z,(PA '\/' PB)) by Th1, PARTIT1:16;

theorem :: BVFUNC11:3
for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) c= EqClass (z,PA) by Th1, PARTIT1:15;

theorem :: BVFUNC11:4
for Y being non empty set
for z being Element of Y
for PA being a_partition of Y holds
( EqClass (z,PA) c= EqClass (z,(%O Y)) &amp; EqClass (z,(%I Y)) c= EqClass (z,PA) ) by Th1, PARTIT1:32;

theorem :: BVFUNC11:5
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent &amp; G = {A,B} &amp; A <> B holds
for a, b being set st a in A &amp; b in B holds
a meets b
proofend;

theorem :: BVFUNC11:6
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent &amp; G = {A,B} &amp; A <> B holds
'/\' G = A '/\' B
proofend;

theorem :: BVFUNC11:7
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G = {A,B} &amp; A <> B holds
CompF (A,G) = B
proofend;

begin

theorem Th8: :: BVFUNC11:8
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A being a_partition of Y st a '<' b holds
All (a,A,G) '<' Ex (b,A,G)
proofend;

theorem Th9: :: BVFUNC11:9
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G)
proofend;

theorem :: BVFUNC11:10
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
proofend;

theorem :: BVFUNC11:11
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G)
proofend;

theorem :: BVFUNC11:12
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
proofend;

theorem Th13: :: BVFUNC11:13
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)
proofend;

theorem Th14: :: BVFUNC11:14
for Y being non empty set
for a being Function of 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 ((Ex (('not' a),B,G)),A,G)
proofend;

theorem Th15: :: BVFUNC11:15
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G)
proofend;

theorem :: BVFUNC11:16
for Y being non empty set
for a being Function of 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 ((Ex (('not' a),B,G)),A,G)
proofend;

theorem :: BVFUNC11:17
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G)
proofend;

theorem :: BVFUNC11:18
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G)
proofend;

:: from BVFUNC12
theorem Th19: :: BVFUNC11:19
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G)
proofend;

theorem Th20: :: BVFUNC11:20
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G)
proofend;

theorem Th21: :: BVFUNC11:21
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G)
proofend;

theorem :: BVFUNC11:22
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
proofend;

theorem :: BVFUNC11:23
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G)
proofend;

theorem :: BVFUNC11:24
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)
proofend;

theorem :: BVFUNC11:25
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)
proofend;

:: BVFUNC13
theorem Th26: :: BVFUNC11:26
for Y being non empty set
for a being Function of 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))
proofend;

theorem Th27: :: BVFUNC11:27
for Y being non empty set
for a being Function of 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))
proofend;

theorem Th28: :: BVFUNC11:28
for Y being non empty set
for a being Function of 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))
proofend;

theorem Th29: :: BVFUNC11:29
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:30
for Y being non empty set
for a being Function of 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))
proofend;

theorem Th31: :: BVFUNC11:31
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:32
for Y being non empty set
for a being Function of 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)) by PARTIT_2:11, PARTIT_2:17;

theorem Th33: :: BVFUNC11:33
for Y being non empty set
for a being Function of 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))
proofend;

theorem Th34: :: BVFUNC11:34
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:35
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:36
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:37
for Y being non empty set
for a being Function of 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))
proofend;

theorem Th38: :: BVFUNC11:38
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th39: :: BVFUNC11:39
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th40: :: BVFUNC11:40
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th41: :: BVFUNC11:41
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th42: :: BVFUNC11:42
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th43: :: BVFUNC11:43
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th44: :: BVFUNC11:44
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th45: :: BVFUNC11:45
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th46: :: BVFUNC11:46
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th47: :: BVFUNC11:47
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th48: :: BVFUNC11:48
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th49: :: BVFUNC11:49
for Y being non empty set
for a being Function of 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)
proofend;

theorem Th50: :: BVFUNC11:50
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:51
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:52
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:53
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:54
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:55
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:56
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:57
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:58
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:59
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:60
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:61
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:62
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:63
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:64
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:65
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:66
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:67
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:68
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:69
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:70
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:71
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:72
for Y being non empty set
for a being Function of 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))
proofend;

theorem :: BVFUNC11:73
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:74
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:75
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:76
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:77
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:78
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:79
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:80
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:81
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: BVFUNC11:82
for Y being non empty set
for a being Function of 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)
proofend;