:: BVFUNC_2 semantic presentation

begin


definition
let X be set ;
:: original: PARTITIONS
redefine func PARTITIONS X ->  Part-Family of X;
coherence
 PARTITIONS X is Part-Family of X
proof
A1: PARTITIONS X c= bool (bool X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PARTITIONS X or x in bool (bool X) )
assume  x in PARTITIONS X ; ::_thesis: x in bool (bool X)
then  x is a_partition of X by PARTIT1:def_3;
hence  x in bool (bool X) ; ::_thesis: verum
end;
 for S being set st S in PARTITIONS X holds
S is a_partition of X by PARTIT1:def_3;
hence  PARTITIONS X is Part-Family of X by A1, EQREL_1:def_7; ::_thesis: verum
end;
end;

definition
let X be set ;
let F be non empty Part-Family of X;
:: original: Element
redefine mode Element of F ->  a_partition of X;
coherence
 for b1 being Element of F holds b1 is a_partition of X by EQREL_1:def_7;
end;

theorem Th1: :: BVFUNC_2:1
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for y being Element of Y ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for y being Element of Y ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
let G be Subset of (PARTITIONS Y); ::_thesis: for y being Element of Y ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
let y be Element of Y; ::_thesis: ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
deffunc H1( Element of PARTITIONS Y) ->  Element of $1 = EqClass (y,$1);
defpred S1[ set ] means $1 in G;
consider h being PartFunc of (PARTITIONS Y),(bool Y) such that
A1: for d being Element of PARTITIONS Y holds
( d in dom h iff S1[d] ) and
A2: for d being Element of PARTITIONS Y st d in dom h holds
h /. d = H1(d) from PARTFUN2:sch_2();
A3: G c= dom h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in dom h )
assume  x in G ; ::_thesis: x in dom h
hence  x in dom h by A1; ::_thesis: verum
end;
A4: for d being set st d in G holds
h . d in d
proof
let d be set ; ::_thesis: ( d in G implies h . d in d )
assume A5: d in G ; ::_thesis: h . d in d
then reconsider d = d as a_partition of Y by PARTIT1:def_3;
 h /. d = h . d by A3, A5, PARTFUN1:def_6;
then  h . d = EqClass (y,d) by A2, A3, A5;
hence  h . d in d ; ::_thesis: verum
end;
 dom h c= G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom h or x in G )
assume  x in dom h ; ::_thesis: x in G
hence  x in G by A1; ::_thesis: verum
end;
then A6: dom h = G by A3, XBOOLE_0:def_10;
reconsider rr = rng h as Subset-Family of Y ;
A7: for d being Element of PARTITIONS Y st d in dom h holds
y in h . d
proof
let d be Element of PARTITIONS Y; ::_thesis: ( d in dom h implies y in h . d )
assume A8: d in dom h ; ::_thesis: y in h . d
then  h /. d = EqClass (y,d) by A2;
then  h . d = EqClass (y,d) by A8, PARTFUN1:def_6;
hence  y in h . d by EQREL_1:def_6; ::_thesis: verum
end;
A9: for c being set st c in rng h holds
y in c
proof
let c be set ; ::_thesis: ( c in rng h implies y in c )
assume  c in rng h ; ::_thesis: y in c
then  ex a being set st
( a in dom h & c = h . a ) by FUNCT_1:def_3;
hence  y in c by A7; ::_thesis: verum
end;
percases ( rng h = {} or rng h <> {} ) ;
suppose rng h = {} ; ::_thesis: ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
then  Intersect rr = Y by SETFAM_1:def_9;
hence  ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) ) by A6, A4; ::_thesis: verum
end;
suppose rng h <> {} ; ::_thesis: ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) )
then  ( y in meet (rng h) & Intersect rr = meet (rng h) ) by A9, SETFAM_1:def_1, SETFAM_1:def_9;
hence  ex X being Subset of Y st
( y in X & ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & X = Intersect F & X <> {} ) ) by A6, A4; ::_thesis: verum
end;
end;
end;

definition
let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
func '/\' G ->  a_partition of Y means :Def1: :: BVFUNC_2:def 1
 for x being set holds
( x in it iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) );
existence
 ex b1 being a_partition of Y st
for x being set holds
( x in b1 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) )
proof
defpred S1[ set ] means  ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & $1 = Intersect F & $1 <> {} );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool Y & S1[x] ) ) from XBOOLE_0:sch_1();
A2: for A being Subset of Y st A in X holds
( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) ) )
assume  A in X ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
then consider h1 being Function, F1 being Subset-Family of Y such that
A3: dom h1 = G and
A4: rng h1 = F1 and
A5: for d being set st d in G holds
h1 . d in d and
A6: A = Intersect F1 and
A7: A <> {} by A1;
thus  A <> {} by A7; ::_thesis: for B being Subset of Y holds
( not B in X or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in X or A = B or A misses B )
assume  B in X ; ::_thesis: ( A = B or A misses B )
then consider h2 being Function, F2 being Subset-Family of Y such that
A8: dom h2 = G and
A9: rng h2 = F2 and
A10: for d being set st d in G holds
h2 . d in d and
A11: B = Intersect F2 and
 B <> {} by A1;
percases ( G = {} or G <> {} ) ;
supposeA12: G = {} ; ::_thesis: ( A = B or A misses B )
then  rng h1 = {} by A3, RELAT_1:42;
hence  ( A = B or A misses B ) by A4, A6, A8, A9, A11, A12, RELAT_1:42; ::_thesis: verum
end;
supposeA13: G <> {} ; ::_thesis: ( A = B or A misses B )
now__::_thesis:_(_not_A_meets_B_or_A_=_B_or_A_misses_B_)
assume  A meets B ; ::_thesis: ( A = B or A misses B )
then consider p being set  such that
A16: p in A and
A17: p in B by XBOOLE_0:3;
A18: p in meet (rng h2) by A9, A11, A13, A17, SETFAM_1:def_9, A8, RELAT_1:42;
A19: p in meet (rng h1) by A4, A6, A3, A13, RELAT_1:42, A16, SETFAM_1:def_9;
 for g being set st g in G holds
h1 . g = h2 . g
proof
let g be set ; ::_thesis: ( g in G implies h1 . g = h2 . g )
assume A20: g in G ; ::_thesis: h1 . g = h2 . g
then reconsider g = g as a_partition of Y by PARTIT1:def_3;
 h1 . g in rng h1 by A3, A20, FUNCT_1:def_3;
then A21: p in h1 . g by A19, SETFAM_1:def_1;
 h2 . g in rng h2 by A8, A20, FUNCT_1:def_3;
then A22: p in h2 . g by A18, SETFAM_1:def_1;
 ( h1 . g in g & h2 . g in g ) by A5, A10, A20;
hence  h1 . g = h2 . g by A21, A22, XBOOLE_0:3, EQREL_1:def_4; ::_thesis: verum
end;
hence  ( A = B or A misses B ) by A3, A4, A6, A8, A9, A11, FUNCT_1:2; ::_thesis: verum
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
end;
end;
A23: Y c= union X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in union X )
assume  y in Y ; ::_thesis: y in union X
then reconsider y = y as Element of Y ;
consider a being Subset of Y such that
A24: y in a and
A25: ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & a = Intersect F & a <> {} ) by Th1;
 a in X by A1, A25;
hence  y in union X by A24, TARSKI:def_4; ::_thesis: verum
end;
B28: union X c= Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union X or a in Y )
assume  a in union X ; ::_thesis: a in Y
then consider p being set  such that
A26: a in p and
A27: p in X by TARSKI:def_4;
 ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & p = Intersect F & p <> {} ) by A1, A27;
hence  a in Y by A26; ::_thesis: verum
end;
take  X ; ::_thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
( x in X iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ) )
 X c= bool Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in bool Y )
assume  a in X ; ::_thesis: a in bool Y
hence  a in bool Y by A1; ::_thesis: verum
end;
then reconsider X = X as Subset-Family of Y ;
 X is a_partition of Y by B28, A2, EQREL_1:def_4, A23, XBOOLE_0:def_10;
hence  ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
( x in X iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being a_partition of Y st ( for x being set holds
( x in b1 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ) & ( for x being set holds
( x in b2 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ) holds
b1 = b2
proof
let A1, A2 be a_partition of Y; ::_thesis: ( ( for x being set holds
( x in A1 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ) & ( for x being set holds
( x in A2 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ) implies A1 = A2 )
assume that
A29: for x being set holds
( x in A1 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) and
A30: for x being set holds
( x in A2 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) ; ::_thesis: A1 = A2
now__::_thesis:_for_y_being_set_holds_
(_y_in_A1_iff_y_in_A2_)
let y be set ; ::_thesis: ( y in A1 iff y in A2 )
 ( y in A1 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & y = Intersect F & y <> {} ) ) by A29;
hence  ( y in A1 iff y in A2 ) by A30; ::_thesis: verum
end;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines '/\' BVFUNC_2:def_1_:_
 for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b3 being a_partition of Y holds
( b3 = '/\' G iff for x being set holds
( x in b3 iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) );

definition
let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
let b be set ;
predb is_upper_min_depend_of G means :Def2: :: BVFUNC_2:def 2
( ( for d being a_partition of Y st d in G holds
b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) holds
e = b ) );
end;

:: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def_2_:_
 for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b being set holds
( b is_upper_min_depend_of G iff ( ( for d being a_partition of Y st d in G holds
b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) holds
e = b ) ) );

theorem Th2: :: BVFUNC_2:2
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
let G be Subset of (PARTITIONS Y); ::_thesis: for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
let y be Element of Y; ::_thesis: ( G <> {} implies ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G ) )
defpred S1[ set ] means ( y in $1 & ( for d being a_partition of Y st d in G holds
$1 is_a_dependent_set_of d ) );
reconsider XX =  {  X where X is Subset of Y : S1[X]  }  as Subset-Family of Y from DOMAIN_1:sch_7();
reconsider XX = XX as Subset-Family of Y ;
assume  G <> {} ; ::_thesis: ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
then consider g being set  such that
A1: g in G by XBOOLE_0:def_1;
reconsider g = g as a_partition of Y by A1, PARTIT1:def_3;
A2: union g = Y by EQREL_1:def_4;
take  Intersect XX ; ::_thesis: ( y in Intersect XX & Intersect XX is_upper_min_depend_of G )
 ( Y c= Y & ( for d being a_partition of Y st d in G holds
Y is_a_dependent_set_of d ) ) by PARTIT1:7;
then A3: Y in XX ;
A4: for A being set st A in g holds
( A <> {} & ( for B being set holds
( not B in g or A = B or A misses B ) ) ) by EQREL_1:def_4;
A5: for e being set st e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) holds
e = Intersect XX
proof
let e be set ; ::_thesis: ( e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) implies e = Intersect XX )
assume that
A6: e c= Intersect XX and
A7: for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ; ::_thesis: e = Intersect XX
consider Ad being set  such that
A8: Ad c= g and
A9: Ad <> {} and
A10: e = union Ad by PARTIT1:def_1, A1, A7;
A11: e c= Y by A2, A8, A10, ZFMISC_1:77;
percases ( y in e or not y in e ) ;
suppose y in e ; ::_thesis: e = Intersect XX
then A12: e in XX by A7, A11;
 Intersect XX c= e
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in Intersect XX or X1 in e )
assume  X1 in Intersect XX ; ::_thesis: X1 in e
then  X1 in meet XX by A3, SETFAM_1:def_9;
hence  X1 in e by A12, SETFAM_1:def_1; ::_thesis: verum
end;
hence  e = Intersect XX by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA13: not y in e ; ::_thesis: e = Intersect XX
reconsider e = e as Subset of Y by A2, A8, A10, ZFMISC_1:77;
 e ` = Y \ e by SUBSET_1:def_4;
then A14: y in e ` by A13, XBOOLE_0:def_5;
 e <> Y by A13;
then  for d being a_partition of Y st d in G holds
e ` is_a_dependent_set_of d by A7, PARTIT1:10;
then A15: e ` in XX by A14;
A16: Intersect XX c= e `
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in Intersect XX or X1 in e ` )
assume  X1 in Intersect XX ; ::_thesis: X1 in e `
then  X1 in meet XX by A3, SETFAM_1:def_9;
hence  X1 in e ` by A15, SETFAM_1:def_1; ::_thesis: verum
end;
A17: e /\ e = e ;
consider ad being set  such that
A18: ad in Ad by A9, XBOOLE_0:def_1;
 e /\ (e `) = {} by XBOOLE_0:def_7, SUBSET_1:24;
then  e /\ (Intersect XX) = {} by A16, XBOOLE_1:3, XBOOLE_1:26;
then  e c= {} by A6, A17, XBOOLE_1:26;
then  union Ad = {} by A10;
then A19: ad c= {} by A18, ZFMISC_1:74;
 ad <> {} by A4, A8, A18;
hence  e = Intersect XX by A19; ::_thesis: verum
end;
end;
end;
 for X1 being set st X1 in XX holds
y in X1
proof
let X1 be set ; ::_thesis: ( X1 in XX implies y in X1 )
assume  X1 in XX ; ::_thesis: y in X1
then  ex X being Subset of Y st
( X = X1 & y in X & ( for d being a_partition of Y st d in G holds
X is_a_dependent_set_of d ) ) ;
hence  y in X1 ; ::_thesis: verum
end;
then A20: y in meet XX by A3, SETFAM_1:def_1;
then A21: Intersect XX <> {} by SETFAM_1:def_9;
 for d being a_partition of Y st d in G holds
Intersect XX is_a_dependent_set_of d
proof
let d be a_partition of Y; ::_thesis: ( d in G implies Intersect XX is_a_dependent_set_of d )
assume A22: d in G ; ::_thesis: Intersect XX is_a_dependent_set_of d
 for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of d
proof
let X1 be set ; ::_thesis: ( X1 in XX implies X1 is_a_dependent_set_of d )
assume  X1 in XX ; ::_thesis: X1 is_a_dependent_set_of d
then  ex X being Subset of Y st
( X = X1 & y in X & ( for d being a_partition of Y st d in G holds
X is_a_dependent_set_of d ) ) ;
hence  X1 is_a_dependent_set_of d by A22; ::_thesis: verum
end;
hence  Intersect XX is_a_dependent_set_of d by A21, PARTIT1:8; ::_thesis: verum
end;
hence  ( y in Intersect XX & Intersect XX is_upper_min_depend_of G ) by A3, A20, A5, Def2, SETFAM_1:def_9; ::_thesis: verum
end;

definition
let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
func '\/' G ->  a_partition of Y means :Def3: :: BVFUNC_2:def 3
 for x being set holds
( x in it iff x is_upper_min_depend_of G ) if G <> {}
otherwise it = %I Y;
existence
 ( ( G <> {} implies ex b1 being a_partition of Y st
for x being set holds
( x in b1 iff x is_upper_min_depend_of G ) ) & ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y ) )
proof
thus  ( G <> {} implies ex X being a_partition of Y st
for x being set holds
( x in X iff x is_upper_min_depend_of G ) ) ::_thesis: ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y )
proof
defpred S1[ set ] means $1 is_upper_min_depend_of G;
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool Y & S1[x] ) ) from XBOOLE_0:sch_1();
A2: union X c= Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union X or y in Y )
assume  y in union X ; ::_thesis: y in Y
then consider a being set  such that
A3: y in a and
A4: a in X by TARSKI:def_4;
 a in bool Y by A1, A4;
hence  y in Y by A3; ::_thesis: verum
end;
assume A5: G <> {} ; ::_thesis: ex X being a_partition of Y st
for x being set holds
( x in X iff x is_upper_min_depend_of G )
then consider g being set  such that
A6: g in G by XBOOLE_0:def_1;
reconsider g = g as a_partition of Y by A6, PARTIT1:def_3;
A7: union g = Y by EQREL_1:def_4;
A8: for x being set holds
( x in X iff x is_upper_min_depend_of G )
proof
let x be set ; ::_thesis: ( x in X iff x is_upper_min_depend_of G )
 for x being set st x is_upper_min_depend_of G holds
x in bool Y
proof
let x be set ; ::_thesis: ( x is_upper_min_depend_of G implies x in bool Y )
assume  x is_upper_min_depend_of G ; ::_thesis: x in bool Y
then  ex A being set st
( A c= g & A <> {} & x = union A ) by PARTIT1:def_1, A6, Def2;
then  x c= union g by ZFMISC_1:77;
hence  x in bool Y by A7; ::_thesis: verum
end;
hence  ( x in X iff x is_upper_min_depend_of G ) by A1; ::_thesis: verum
end;
B11: Y c= union X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in union X )
assume  y in Y ; ::_thesis: y in union X
then reconsider y = y as Element of Y ;
consider a being Subset of Y such that
A9: y in a and
A10: a is_upper_min_depend_of G by A5, Th2;
 a in X by A8, A10;
hence  y in union X by A9, TARSKI:def_4; ::_thesis: verum
end;
A12: for A being set st A in g holds
( A <> {} & ( for B being set holds
( not B in g or A = B or A misses B ) ) ) by EQREL_1:def_4;
A13: for A being Subset of Y st A in X holds
( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) ) )
assume  A in X ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
then A14: A is_upper_min_depend_of G by A8;
then consider Aa being set  such that
A15: Aa c= g and
A16: Aa <> {} and
A17: A = union Aa by PARTIT1:def_1, A6, Def2;
consider aa being set  such that
A18: aa in Aa by A16, XBOOLE_0:def_1;
A19: aa c= union Aa by A18, ZFMISC_1:74;
 aa <> {} by A12, A15, A18;
hence  A <> {} by A17, A19; ::_thesis: for B being Subset of Y holds
( not B in X or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in X or A = B or A misses B )
assume  B in X ; ::_thesis: ( A = B or A misses B )
then A20: B is_upper_min_depend_of G by A8;
now__::_thesis:_(_A_meets_B_implies_A_=_B_)
assume A21: A meets B ; ::_thesis: A = B
A22: for d being a_partition of Y st d in G holds
A /\ B is_a_dependent_set_of d
proof
let d be a_partition of Y; ::_thesis: ( d in G implies A /\ B is_a_dependent_set_of d )
assume  d in G ; ::_thesis: A /\ B is_a_dependent_set_of d
then  ( A is_a_dependent_set_of d & B is_a_dependent_set_of d ) by A14, A20, Def2;
hence  A /\ B is_a_dependent_set_of d by A21, PARTIT1:9; ::_thesis: verum
end;
A23: A /\ B = B by A20, A22, Def2, XBOOLE_1:17;
A24: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume  x in B ; ::_thesis: x in A
hence  x in A by A23, XBOOLE_0:def_4; ::_thesis: verum
end;
A25: A /\ B = A by A14, A22, Def2, XBOOLE_1:17;
 A c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume  x in A ; ::_thesis: x in B
hence  x in B by A25, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  A = B by A24, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
take  X ; ::_thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
( x in X iff x is_upper_min_depend_of G ) ) )
 X c= bool Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool Y )
assume  x in X ; ::_thesis: x in bool Y
hence  x in bool Y by A1; ::_thesis: verum
end;
then reconsider X = X as Subset-Family of Y ;
 X is a_partition of Y by B11, A13, EQREL_1:def_4, A2, XBOOLE_0:def_10;
hence  ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
( x in X iff x is_upper_min_depend_of G ) ) ) by A8; ::_thesis: verum
end;
thus  ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being a_partition of Y holds
( ( G <> {} & ( for x being set holds
( x in b1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in b2 iff x is_upper_min_depend_of G ) ) implies b1 = b2 ) & ( not G <> {} & b1 = %I Y & b2 = %I Y implies b1 = b2 ) )
proof
let A1, A2 be a_partition of Y; ::_thesis: ( ( G <> {} & ( for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 ) & ( not G <> {} & A1 = %I Y & A2 = %I Y implies A1 = A2 ) )
now__::_thesis:_(_G_<>_{}_&_(_for_x_being_set_holds_
(_x_in_A1_iff_x_is_upper_min_depend_of_G_)_)_&_(_for_x_being_set_holds_
(_x_in_A2_iff_x_is_upper_min_depend_of_G_)_)_implies_A1_=_A2_)
assume that
 G <> {} and
A26: for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) and
A27: for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ; ::_thesis: A1 = A2
 for y being set holds
( y in A1 iff y in A2 ) by A27, A26;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
hence  ( ( G <> {} & ( for x being set holds
( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds
( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 ) & ( not G <> {} & A1 = %I Y & A2 = %I Y implies A1 = A2 ) ) ; ::_thesis: verum
end;
consistency
 for b1 being a_partition of Y holds verum ;
end;

:: deftheorem Def3 defines '\/' BVFUNC_2:def_3_:_
 for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b3 being a_partition of Y holds
( ( G <> {} implies ( b3 = '\/' G iff for x being set holds
( x in b3 iff x is_upper_min_depend_of G ) ) ) & ( not G <> {} implies ( b3 = '\/' G iff b3 = %I Y ) ) );

theorem :: BVFUNC_2:3
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st PA in G holds
PA '>' '/\' G
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st PA in G holds
PA '>' '/\' G
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st PA in G holds
PA '>' '/\' G
let PA be a_partition of Y; ::_thesis: ( PA in G implies PA '>' '/\' G )
assume A1: PA in G ; ::_thesis: PA '>' '/\' G
 for x being set st x in '/\' G holds
ex a being set st
( a in PA & x c= a )
proof
let x be set ; ::_thesis: ( x in '/\' G implies ex a being set st
( a in PA & x c= a ) )
assume  x in '/\' G ; ::_thesis: ex a being set st
( a in PA & x c= a )
then consider h being Function, F being Subset-Family of Y such that
A2: dom h = G and
A3: rng h = F and
A4: for d being set st d in G holds
h . d in d and
A5: x = Intersect F and
 x <> {} by Def1;
set a = h . PA;
A6: h . PA in PA by A1, A4;
A7: h . PA in rng h by A1, A2, FUNCT_1:def_3;
then  Intersect F = meet F by A3, SETFAM_1:def_9;
hence  ex a being set st
( a in PA & x c= a ) by A3, A5, A6, A7, SETFAM_1:3; ::_thesis: verum
end;
hence  PA '>' '/\' G by SETFAM_1:def_2; ::_thesis: verum
end;

theorem :: BVFUNC_2:4
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st PA in G holds
PA '<' '\/' G
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st PA in G holds
PA '<' '\/' G
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st PA in G holds
PA '<' '\/' G
let PA be a_partition of Y; ::_thesis: ( PA in G implies PA '<' '\/' G )
assume A1: PA in G ; ::_thesis: PA '<' '\/' G
 for a being set st a in PA holds
ex b being set st
( b in '\/' G & a c= b )
proof
let a be set ; ::_thesis: ( a in PA implies ex b being set st
( b in '\/' G & a c= b ) )
set x = the Element of a;
A2: union ('\/' G) = Y by EQREL_1:def_4;
assume A3: a in PA ; ::_thesis: ex b being set st
( b in '\/' G & a c= b )
then A4: a <> {} by EQREL_1:def_4;
then  the Element of a in Y by A3, TARSKI:def_3;
then consider b being set  such that
A5: the Element of a in b and
A6: b in '\/' G by A2, TARSKI:def_4;
 b is_upper_min_depend_of G by A1, A6, Def3;
then consider B being set  such that
A7: B c= PA and
 B <> {} and
A8: b = union B by PARTIT1:def_1, A1, Def2;
 a in B
proof
consider u being set  such that
A9: the Element of a in u and
A10: u in B by A5, A8, TARSKI:def_4;
B11: a /\ u <> {} by A4, A9, XBOOLE_0:def_4;
 u in PA by A7, A10;
hence  a in B by A3, A10, B11, EQREL_1:def_4, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  ex b being set st
( b in '\/' G & a c= b ) by A6, A8, ZFMISC_1:74; ::_thesis: verum
end;
hence  PA '<' '\/' G by SETFAM_1:def_2; ::_thesis: verum
end;

begin

definition
let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
attrG is generating  means :: BVFUNC_2:def 4
 '/\' G = %I Y;
end;

:: deftheorem  defines generating BVFUNC_2:def_4_:_
 for Y being non empty set
for G being Subset of (PARTITIONS Y) holds
( G is generating iff '/\' G = %I Y );

definition
let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
attrG is independent  means :: BVFUNC_2:def 5
 for h being Function
for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) holds
Intersect F <> {} ;
end;

:: deftheorem  defines independent BVFUNC_2:def_5_:_
 for Y being non empty set
for G being Subset of (PARTITIONS Y) holds
( G is independent iff for h being Function
for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) holds
Intersect F <> {} );

definition
let Y be non empty set ;
let G be Subset of (PARTITIONS Y);
predG is_a_coordinate  means :: BVFUNC_2:def 6
( G is independent & G is generating );
end;

:: deftheorem  defines is_a_coordinate BVFUNC_2:def_6_:_
 for Y being non empty set
for G being Subset of (PARTITIONS Y) holds
( G is_a_coordinate iff ( G is independent & G is generating ) );

definition
let Y be non empty set ;
let PA be a_partition of Y;
:: original: {
redefine func{PA} ->  Subset of (PARTITIONS Y);
coherence
 {PA} is Subset of (PARTITIONS Y)
proof
 PA in PARTITIONS Y by PARTIT1:def_3;
hence  {PA} is Subset of (PARTITIONS Y) by ZFMISC_1:31; ::_thesis: verum
end;
end;

definition
let Y be non empty set ;
let PA be a_partition of Y;
let G be Subset of (PARTITIONS Y);
func CompF (PA,G) ->  a_partition of Y equals :: BVFUNC_2:def 7
 '/\' (G \ {PA});
correctness
coherence
'/\' (G \ {PA}) is a_partition of Y;
;
end;

:: deftheorem  defines CompF BVFUNC_2:def_7_:_
 for Y being non empty set
for PA being a_partition of Y
for G being Subset of (PARTITIONS Y) holds CompF (PA,G) = '/\' (G \ {PA});

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
preda is_independent_of PA,G means :Def8: :: BVFUNC_2:def 8
a is_dependent_of CompF (PA,G);
end;

:: deftheorem Def8 defines is_independent_of BVFUNC_2:def_8_:_
 for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds
( a is_independent_of PA,G iff a is_dependent_of CompF (PA,G) );

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
func All (a,PA,G) ->  Function of Y,BOOLEAN equals :: BVFUNC_2:def 9
 B_INF (a,(CompF (PA,G)));
correctness
coherence
B_INF (a,(CompF (PA,G))) is Function of Y,BOOLEAN;
;
end;

:: deftheorem  defines All BVFUNC_2:def_9_:_
 for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All (a,PA,G) = B_INF (a,(CompF (PA,G)));

definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let G be Subset of (PARTITIONS Y);
let PA be a_partition of Y;
func Ex (a,PA,G) ->  Function of Y,BOOLEAN equals :: BVFUNC_2:def 10
 B_SUP (a,(CompF (PA,G)));
correctness
coherence
B_SUP (a,(CompF (PA,G))) is Function of Y,BOOLEAN;
;
end;

:: deftheorem  defines Ex BVFUNC_2:def_10_:_
 for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds Ex (a,PA,G) = B_SUP (a,(CompF (PA,G)));

theorem :: BVFUNC_2:5
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)
let PA be a_partition of Y; ::_thesis: All (a,PA,G) is_dependent_of CompF (PA,G)
let F be set ; :: according to BVFUNC_1:def_15 ::_thesis: ( not F in CompF (PA,G) or for b1, b2 being set holds
( not b1 in F or not b2 in F or (All (a,PA,G)) . b1 = (All (a,PA,G)) . b2 ) )
assume A1: F in CompF (PA,G) ; ::_thesis: for b1, b2 being set holds
( not b1 in F or not b2 in F or (All (a,PA,G)) . b1 = (All (a,PA,G)) . b2 )
thus  for x1, x2 being set st x1 in F & x2 in F holds
(All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 ::_thesis: verum
proof
let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 )
assume A2: ( x1 in F & x2 in F ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;
A3: x2 in EqClass (x2,(CompF (PA,G))) by EQREL_1:def_6;
 ( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by A1, EQREL_1:def_4;
then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by A2, A3, EQREL_1:def_6, XBOOLE_0:3;
percases ( ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ) ;
supposeA5: ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
then  (All (a,PA,G)) . x2 = TRUE by BVFUNC_1:def_16;
hence  (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A5, BVFUNC_1:def_16; ::_thesis: verum
end;
suppose ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
hence  (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A4; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
hence  (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A4; ::_thesis: verum
end;
supposeA6: ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
then  (All (a,PA,G)) . x2 = FALSE by BVFUNC_1:def_16;
hence  (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A6, BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;
end;

theorem :: BVFUNC_2:6
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G)
let PA be a_partition of Y; ::_thesis: Ex (a,PA,G) is_dependent_of CompF (PA,G)
let F be set ; :: according to BVFUNC_1:def_15 ::_thesis: ( not F in CompF (PA,G) or for b1, b2 being set holds
( not b1 in F or not b2 in F or (Ex (a,PA,G)) . b1 = (Ex (a,PA,G)) . b2 ) )
assume A1: F in CompF (PA,G) ; ::_thesis: for b1, b2 being set holds
( not b1 in F or not b2 in F or (Ex (a,PA,G)) . b1 = (Ex (a,PA,G)) . b2 )
thus  for x1, x2 being set st x1 in F & x2 in F holds
(Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 ::_thesis: verum
proof
let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 )
assume A2: ( x1 in F & x2 in F ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;
A3: x2 in EqClass (x2,(CompF (PA,G))) by EQREL_1:def_6;
 ( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by A1, EQREL_1:def_4;
then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by A2, A3, EQREL_1:def_6, XBOOLE_0:3;
percases ( ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) or ( ( for x being Element of Y holds
( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) or ( ( for x being Element of Y holds
( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ;
supposeA5: ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2
then  (B_SUP (a,(CompF (PA,G)))) . x1 = TRUE by BVFUNC_1:def_17;
hence  (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A5, BVFUNC_1:def_17; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2
hence  (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A4; ::_thesis: verum
end;
suppose ( ( for x being Element of Y holds
( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2
hence  (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A4; ::_thesis: verum
end;
supposeA6: ( ( for x being Element of Y holds
( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2
then  (B_SUP (a,(CompF (PA,G)))) . x1 = FALSE by BVFUNC_1:def_17;
hence  (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A6, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
end;

theorem :: BVFUNC_2:7
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y
let PA be a_partition of Y; ::_thesis: All ((I_el Y),PA,G) = I_el Y
 for z being Element of Y holds (All ((I_el Y),PA,G)) . z = TRUE
proof
let z be Element of Y; ::_thesis: (All ((I_el Y),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(I_el Y) . x = TRUE by BVFUNC_1:def_11;
hence  (All ((I_el Y),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
hence  All ((I_el Y),PA,G) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_2:8
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y
let PA be a_partition of Y; ::_thesis: Ex ((I_el Y),PA,G) = I_el Y
 for z being Element of Y holds (Ex ((I_el Y),PA,G)) . z = TRUE
proof
let z be Element of Y; ::_thesis: (Ex ((I_el Y),PA,G)) . z = TRUE
 ( z in EqClass (z,(CompF (PA,G))) & (I_el Y) . z = TRUE ) by BVFUNC_1:def_11, EQREL_1:def_6;
hence  (Ex ((I_el Y),PA,G)) . z = TRUE by BVFUNC_1:def_17; ::_thesis: verum
end;
hence  Ex ((I_el Y),PA,G) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_2:9
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y
let PA be a_partition of Y; ::_thesis: All ((O_el Y),PA,G) = O_el Y
 for z being Element of Y holds (All ((O_el Y),PA,G)) . z = FALSE
proof
let z be Element of Y; ::_thesis: (All ((O_el Y),PA,G)) . z = FALSE
 ( z in EqClass (z,(CompF (PA,G))) & (O_el Y) . z = FALSE ) by BVFUNC_1:def_10, EQREL_1:def_6;
hence  (All ((O_el Y),PA,G)) . z = FALSE by BVFUNC_1:def_16; ::_thesis: verum
end;
hence  All ((O_el Y),PA,G) = O_el Y by BVFUNC_1:def_10; ::_thesis: verum
end;

theorem :: BVFUNC_2:10
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y
let PA be a_partition of Y; ::_thesis: Ex ((O_el Y),PA,G) = O_el Y
 for z being Element of Y holds (Ex ((O_el Y),PA,G)) . z = FALSE
proof
let z be Element of Y; ::_thesis: (Ex ((O_el Y),PA,G)) . z = FALSE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(O_el Y) . x <> TRUE by BVFUNC_1:def_10;
hence  (Ex ((O_el Y),PA,G)) . z = FALSE by BVFUNC_1:def_17; ::_thesis: verum
end;
hence  Ex ((O_el Y),PA,G) = O_el Y by BVFUNC_1:def_10; ::_thesis: verum
end;

theorem :: BVFUNC_2:11
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) '<' a
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) '<' a
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) '<' a
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All (a,PA,G) '<' a
let PA be a_partition of Y; ::_thesis: All (a,PA,G) '<' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (a,PA,G)) . z = TRUE or a . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (All (a,PA,G)) . z = TRUE ; ::_thesis: a . z = TRUE
hence  a . z = TRUE by A1, BVFUNC_1:def_16; ::_thesis: verum
end;

theorem :: BVFUNC_2:12
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '<' Ex (a,PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '<' Ex (a,PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '<' Ex (a,PA,G)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a '<' Ex (a,PA,G)
let PA be a_partition of Y; ::_thesis: a '<' Ex (a,PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or (Ex (a,PA,G)) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  a . z = TRUE ; ::_thesis: (Ex (a,PA,G)) . z = TRUE
hence  (Ex (a,PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum
end;

theorem :: BVFUNC_2:13
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G)
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE or (All ((a 'or' b),PA,G)) . z = TRUE )
assume  ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE ; ::_thesis: (All ((a 'or' b),PA,G)) . z = TRUE
then A1: ((All (a,PA,G)) . z) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def_4;
A2: ( (All (b,PA,G)) . z = TRUE or (All (b,PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_(All_(a,PA,G))_._z_=_TRUE_&_(All_((a_'or'_b),PA,G))_._z_=_TRUE_)_or_(_(All_(b,PA,G))_._z_=_TRUE_&_(All_((a_'or'_b),PA,G))_._z_=_TRUE_)_)
percases ( (All (a,PA,G)) . z = TRUE or (All (b,PA,G)) . z = TRUE ) by A1, A2, BINARITH:3;
caseA3: (All (a,PA,G)) . z = TRUE ; ::_thesis: (All ((a 'or' b),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'or' b) . x = TRUE )
assume A4: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'or' b) . x = TRUE
(a 'or' b) . x = (a . x) 'or' (b . x) by BVFUNC_1:def_4
.= TRUE 'or' (b . x) by A3, A4, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ;
hence  (a 'or' b) . x = TRUE ; ::_thesis: verum
end;
hence  (All ((a 'or' b),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
caseA5: (All (b,PA,G)) . z = TRUE ; ::_thesis: (All ((a 'or' b),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'or' b) . x = TRUE )
assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'or' b) . x = TRUE
(a 'or' b) . x = (a . x) 'or' (b . x) by BVFUNC_1:def_4
.= (a . x) 'or' TRUE by A5, A6, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ;
hence  (a 'or' b) . x = TRUE ; ::_thesis: verum
end;
hence  (All ((a 'or' b),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;
hence  (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_2:14
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'imp' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE )
assume A1: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE
A2: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' ((All (b,PA,G)) . z) by BVFUNC_1:def_8;
percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ) ;
suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE
then  (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
then ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
hence  ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum
end;
supposeA3: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: b . x1 <> TRUE ;
A6: a . x1 = TRUE by A3, A4;
(a 'imp' b) . x1 = ('not' (a . x1)) 'or' (b . x1) by BVFUNC_1:def_8
.= ('not' TRUE) 'or' FALSE by A5, A6, XBOOLEAN:def_3
.= FALSE 'or' FALSE by MARGREL1:11
.= FALSE ;
hence  ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE by A1, A4, BVFUNC_1:def_16; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE
then ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by A2, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ;
hence  ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE
then ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE 'or' ((All (b,PA,G)) . z) by MARGREL1:11, A2, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ;
hence  ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_2:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((a '&' b),PA,G)) . z = TRUE or ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE )
assume  (Ex ((a '&' b),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A1: x1 in EqClass (z,(CompF (PA,G))) and
A2: (a '&' b) . x1 = TRUE by BVFUNC_1:def_17;
A3: (a . x1) '&' (b . x1) = TRUE by A2, MARGREL1:def_20;
then A4: b . x1 = TRUE by MARGREL1:12;
 a . x1 = TRUE by A3, MARGREL1:12;
then A5: (Ex (a,PA,G)) . z = TRUE by A1, BVFUNC_1:def_17;
((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z) by MARGREL1:def_20
.= TRUE '&' TRUE by A1, A4, A5, BVFUNC_1:def_17
.= TRUE ;
hence  ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_2:16
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G)
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'xor' (Ex (b,PA,G))) . z = TRUE or (Ex ((a 'xor' b),PA,G)) . z = TRUE )
A1: ((Ex (a,PA,G)) 'xor' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) 'xor' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_5
.= (('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z)) 'or' (((Ex (a,PA,G)) . z) '&' ('not' ((Ex (b,PA,G)) . z))) ;
A2: ( ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = TRUE or ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
A3: 'not' FALSE = TRUE by MARGREL1:11;
assume A4: ((Ex (a,PA,G)) 'xor' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a 'xor' b),PA,G)) . z = TRUE
now__::_thesis:_(_(_('not'_((Ex_(a,PA,G))_._z))_'&'_((Ex_(b,PA,G))_._z)_=_TRUE_&_(Ex_((a_'xor'_b),PA,G))_._z_=_TRUE_)_or_(_((Ex_(a,PA,G))_._z)_'&'_('not'_((Ex_(b,PA,G))_._z))_=_TRUE_&_(Ex_((a_'xor'_b),PA,G))_._z_=_TRUE_)_)
percases ( ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = TRUE or ((Ex (a,PA,G)) . z) '&' ('not' ((Ex (b,PA,G)) . z)) = TRUE ) by A4, A1, A2, BINARITH:3;
caseA5: ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'xor' b),PA,G)) . z = TRUE
then  (Ex (b,PA,G)) . z = TRUE by MARGREL1:12;
then consider x1 being Element of Y such that
A6: x1 in EqClass (z,(CompF (PA,G))) and
A7: b . x1 = TRUE by BVFUNC_1:def_17;
 'not' ((Ex (a,PA,G)) . z) = TRUE by A5, MARGREL1:12;
then  a . x1 <> TRUE by A6, BVFUNC_1:def_17, MARGREL1:11;
then A8: a . x1 = FALSE by XBOOLEAN:def_3;
(a 'xor' b) . x1 = (a . x1) 'xor' (b . x1) by BVFUNC_1:def_5
.= TRUE 'or' FALSE by A3, A7, A8
.= TRUE by BINARITH:10 ;
hence  (Ex ((a 'xor' b),PA,G)) . z = TRUE by A6, BVFUNC_1:def_17; ::_thesis: verum
end;
caseA9: ((Ex (a,PA,G)) . z) '&' ('not' ((Ex (b,PA,G)) . z)) = TRUE ; ::_thesis: (Ex ((a 'xor' b),PA,G)) . z = TRUE
then  (Ex (a,PA,G)) . z = TRUE by MARGREL1:12;
then consider x1 being Element of Y such that
A10: x1 in EqClass (z,(CompF (PA,G))) and
A11: a . x1 = TRUE by BVFUNC_1:def_17;
 'not' ((Ex (b,PA,G)) . z) = TRUE by A9, MARGREL1:12;
then  b . x1 <> TRUE by A10, BVFUNC_1:def_17, MARGREL1:11;
then A12: b . x1 = FALSE by XBOOLEAN:def_3;
(a 'xor' b) . x1 = (a . x1) 'xor' (b . x1) by BVFUNC_1:def_5
.= FALSE 'or' TRUE by A3, A11, A12
.= TRUE by BINARITH:10 ;
hence  (Ex ((a 'xor' b),PA,G)) . z = TRUE by A10, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((a 'xor' b),PA,G)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_2:17
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G)
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE or (Ex ((a 'imp' b),PA,G)) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE
then A2: ('not' ((Ex (a,PA,G)) . z)) 'or' ((Ex (b,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
A3: ( 'not' ((Ex (a,PA,G)) . z) = TRUE or 'not' ((Ex (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_((Ex_(a,PA,G))_._z)_=_TRUE_&_(Ex_((a_'imp'_b),PA,G))_._z_=_TRUE_)_or_(_(Ex_(b,PA,G))_._z_=_TRUE_&_(Ex_((a_'imp'_b),PA,G))_._z_=_TRUE_)_)
percases ( 'not' ((Ex (a,PA,G)) . z) = TRUE or (Ex (b,PA,G)) . z = TRUE ) by A2, A3, BINARITH:3;
case 'not' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE
then A4: a . z <> TRUE by A1, BVFUNC_1:def_17, MARGREL1:11;
(a 'imp' b) . z = ('not' (a . z)) 'or' (b . z) by BVFUNC_1:def_8
.= TRUE 'or' (b . z) by MARGREL1:11, A4, XBOOLEAN:def_3
.= TRUE by BINARITH:10 ;
hence  (Ex ((a 'imp' b),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum
end;
case (Ex (b,PA,G)) . z = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE
then consider x1 being Element of Y such that
A5: x1 in EqClass (z,(CompF (PA,G))) and
A6: b . x1 = TRUE by BVFUNC_1:def_17;
(a 'imp' b) . x1 = ('not' (a . x1)) 'or' (b . x1) by BVFUNC_1:def_8
.= TRUE by A6, BINARITH:10 ;
hence  (Ex ((a 'imp' b),PA,G)) . z = TRUE by A5, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: verum
end;


theorem :: BVFUNC_2:18
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G)
let PA be a_partition of Y; ::_thesis: 'not' (All (a,PA,G)) = Ex (('not' a),PA,G)
let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z
percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) ) ;
supposeA5: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z
then consider x1 being Element of Y such that
A6: x1 in EqClass (z,(CompF (PA,G))) and
A7: ('not' a) . x1 = TRUE ;
 'not' (a . x1) = TRUE by A7, MARGREL1:def_19;
hence  ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A5, A6, MARGREL1:11; ::_thesis: verum
end;
supposeA8: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z
then  (B_INF (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
then A9: ('not' (B_INF (a,(CompF (PA,G))))) . z = 'not' TRUE by MARGREL1:def_19;
 (B_SUP (('not' a),(CompF (PA,G)))) . z = FALSE by A8, BVFUNC_1:def_17;
hence  ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A9, MARGREL1:11; ::_thesis: verum
end;
supposeA10: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then A11: ('not' (B_INF (a,(CompF (PA,G))))) . z = 'not' FALSE by MARGREL1:def_19;
 (B_SUP (('not' a),(CompF (PA,G)))) . z = TRUE by A10, BVFUNC_1:def_17;
hence  ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A11, MARGREL1:11; ::_thesis: verum
end;
supposeA12: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z
then consider x1 being Element of Y such that
A13: x1 in EqClass (z,(CompF (PA,G))) and
A14: a . x1 <> TRUE ;
 ('not' a) . x1 <> TRUE by A12, A13;
then  'not' (a . x1) <> TRUE by MARGREL1:def_19;
hence  ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A14, MARGREL1:11, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_2:19
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let PA be a_partition of Y; ::_thesis: 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z
percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ;
supposeA5: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z
then consider x1 being Element of Y such that
A6: x1 in EqClass (z,(CompF (PA,G))) and
A7: a . x1 = TRUE ;
 ('not' a) . x1 = 'not' TRUE by A7, MARGREL1:def_19;
hence  ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A5, A6, MARGREL1:11; ::_thesis: verum
end;
supposeA8: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z
then  'not' ((B_SUP (a,(CompF (PA,G)))) . z) = TRUE by MARGREL1:11, BVFUNC_1:def_17;
then  ('not' (B_SUP (a,(CompF (PA,G))))) . z = TRUE by MARGREL1:def_19;
hence  ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A8, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA9: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z
then  (B_SUP (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
then A10: ('not' (B_SUP (a,(CompF (PA,G))))) . z = 'not' TRUE by MARGREL1:def_19;
 (B_INF (('not' a),(CompF (PA,G)))) . z = FALSE by A9, BVFUNC_1:def_16;
hence  ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A10, MARGREL1:11; ::_thesis: verum
end;
supposeA11: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z
then consider x1 being Element of Y such that
A12: x1 in EqClass (z,(CompF (PA,G))) and
A13: ('not' a) . x1 <> TRUE ;
 ('not' a) . x1 = FALSE by A13, XBOOLEAN:def_3;
then  'not' (a . x1) = FALSE by MARGREL1:def_19;
hence  ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A11, A12, MARGREL1:11; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_2:20
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) )
assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G))
A2: u 'imp' (All (a,PA,G)) '<' All ((u 'imp' a),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'imp' (All (a,PA,G))) . z = TRUE or (All ((u 'imp' a),PA,G)) . z = TRUE )
assume  (u 'imp' (All (a,PA,G))) . z = TRUE ; ::_thesis: (All ((u 'imp' a),PA,G)) . z = TRUE
then A3: ('not' (u . z)) 'or' ((All (a,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
A4: ( (All (a,PA,G)) . z = TRUE or (All (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(All_((u_'imp'_a),PA,G))_._z_=_TRUE
percases ( (All (a,PA,G)) . z = TRUE or ( (All (a,PA,G)) . z <> TRUE & 'not' (u . z) = TRUE ) ) by A3, A4, BINARITH:3;
supposeA5: (All (a,PA,G)) . z = TRUE ; ::_thesis: (All ((u 'imp' a),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(u 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'imp' a) . x = TRUE )
assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'imp' a) . x = TRUE
(u 'imp' a) . x = ('not' (u . x)) 'or' (a . x) by BVFUNC_1:def_8
.= ('not' (u . x)) 'or' TRUE by A5, A6, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ;
hence  (u 'imp' a) . x = TRUE ; ::_thesis: verum
end;
hence  (All ((u 'imp' a),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA7: ( (All (a,PA,G)) . z <> TRUE & 'not' (u . z) = TRUE ) ; ::_thesis: (All ((u 'imp' a),PA,G)) . z = TRUE
A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(u 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'imp' a) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'imp' a) . x = TRUE
then  ( (u 'imp' a) . x = ('not' (u . x)) 'or' (a . x) & u . x = u . z ) by Z, Def8, A8, BVFUNC_1:def_8, BVFUNC_1:def_15;
hence  (u 'imp' a) . x = TRUE by A7, BINARITH:10; ::_thesis: verum
end;
hence  (All ((u 'imp' a),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;
hence  (All ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: verum
end;
 All ((u 'imp' a),PA,G) '<' u 'imp' (All (a,PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u 'imp' a),PA,G)) . z = TRUE or (u 'imp' (All (a,PA,G))) . z = TRUE )
assume A9: (All ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE
A11: (u 'imp' (All (a,PA,G))) . z = ('not' (u . z)) 'or' ((All (a,PA,G)) . z) by BVFUNC_1:def_8;
percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
'not' (u . x) = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not 'not' (u . x) = TRUE ) ) ) ;
suppose for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE
then  (All (a,PA,G)) . z = TRUE by BVFUNC_1:def_16;
hence  (u 'imp' (All (a,PA,G))) . z = TRUE by A11, BINARITH:10; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
'not' (u . x) = TRUE ) ) ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE
then  'not' (u . z) = TRUE by EQREL_1:def_6;
hence  (u 'imp' (All (a,PA,G))) . z = TRUE by A11, BINARITH:10; ::_thesis: verum
end;
supposeA12: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not 'not' (u . x) = TRUE ) ) ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A13: x1 in EqClass (z,(CompF (PA,G))) and
A14: 'not' (u . x1) <> TRUE ;
consider x2 being Element of Y such that
A15: x2 in EqClass (z,(CompF (PA,G))) and
A16: a . x2 <> TRUE by A12;
 u . x1 = u . x2 by Z, Def8, A13, A15, BVFUNC_1:def_15;
then A17: u . x2 = TRUE by MARGREL1:11, A14, XBOOLEAN:def_3;
 a . x2 = FALSE by A16, XBOOLEAN:def_3;
then  (u 'imp' a) . x2 = ('not' TRUE) 'or' FALSE by A17, BVFUNC_1:def_8;
then (u 'imp' a) . x2 = FALSE 'or' FALSE by MARGREL1:11
.= FALSE ;
hence  (u 'imp' (All (a,PA,G))) . z = TRUE by A9, A15, BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;
hence  All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) by A2, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_2:21
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u )
assume Z: u is_independent_of PA,G ; ::_thesis: All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
A2: (Ex (a,PA,G)) 'imp' u '<' All ((a 'imp' u),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' u) . z = TRUE or (All ((a 'imp' u),PA,G)) . z = TRUE )
A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: (All ((a 'imp' u),PA,G)) . z = TRUE
then A4: ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def_8;
A5: ( 'not' ((Ex (a,PA,G)) . z) = TRUE or 'not' ((Ex (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_u_._z_=_TRUE_&_(All_((a_'imp'_u),PA,G))_._z_=_TRUE_)_or_(_'not'_((Ex_(a,PA,G))_._z)_=_TRUE_&_u_._z_=_FALSE_&_(All_((a_'imp'_u),PA,G))_._z_=_TRUE_)_)
percases ( u . z = TRUE or ( 'not' ((Ex (a,PA,G)) . z) = TRUE & u . z = FALSE ) ) by A4, A5, BINARITH:3, XBOOLEAN:def_3;
caseA6: u . z = TRUE ; ::_thesis: (All ((a 'imp' u),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' u) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' u) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' u) . x = TRUE
then  ( (a 'imp' u) . x = ('not' (a . x)) 'or' (u . x) & u . x = u . z ) by Z, Def8, A3, BVFUNC_1:def_8, BVFUNC_1:def_15;
hence  (a 'imp' u) . x = TRUE by A6, BINARITH:10; ::_thesis: verum
end;
hence  (All ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
caseC: ( 'not' ((Ex (a,PA,G)) . z) = TRUE & u . z = FALSE ) ; ::_thesis: (All ((a 'imp' u),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' u) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' u) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' u) . x = TRUE
then  a . x <> TRUE by C, BVFUNC_1:def_17, MARGREL1:11;
then  ( (a 'imp' u) . x = ('not' (a . x)) 'or' (u . x) & a . x = FALSE ) by BVFUNC_1:def_8, XBOOLEAN:def_3;
then (a 'imp' u) . x = TRUE 'or' (u . x) by MARGREL1:11
.= TRUE by BINARITH:10 ;
hence  (a 'imp' u) . x = TRUE ; ::_thesis: verum
end;
hence  (All ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;
hence  (All ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: verum
end;
 All ((a 'imp' u),PA,G) '<' (Ex (a,PA,G)) 'imp' u
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'imp' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'imp' u) . z = TRUE )
assume A8: (All ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE
A10: ((Ex (a,PA,G)) 'imp' u) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) by BVFUNC_1:def_8;
percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ;
suppose for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE
then ((Ex (a,PA,G)) 'imp' u) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' TRUE by EQREL_1:def_6, A10
.= TRUE by BINARITH:10 ;
hence  ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: verum
end;
supposeA11: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE
then consider x1 being Element of Y such that
A12: x1 in EqClass (z,(CompF (PA,G))) and
A13: u . x1 <> TRUE ;
consider x2 being Element of Y such that
A14: x2 in EqClass (z,(CompF (PA,G))) and
A15: a . x2 = TRUE by A11;
A16: u . x1 = u . x2 by Z, Def8, A12, A14, BVFUNC_1:def_15;
(a 'imp' u) . x2 = ('not' (a . x2)) 'or' (u . x2) by BVFUNC_1:def_8
.= ('not' TRUE) 'or' FALSE by A13, A15, A16, XBOOLEAN:def_3
.= FALSE 'or' FALSE by MARGREL1:11
.= FALSE ;
hence  ((Ex (a,PA,G)) 'imp' u) . z = TRUE by A8, A14, BVFUNC_1:def_16; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE
then ((Ex (a,PA,G)) 'imp' u) . z = ('not' FALSE) 'or' (u . z) by A10, BVFUNC_1:def_17
.= TRUE 'or' (u . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
hence  ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u by A2, BVFUNC_1:15; ::_thesis: verum
end;

theorem Th22: :: BVFUNC_2:22
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) )
assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G))
let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z
A6: (u 'or' (B_INF (a,(CompF (PA,G))))) . z = (u . z) 'or' ((B_INF (a,(CompF (PA,G)))) . z) by BVFUNC_1:def_4;
percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ) ;
supposeA7: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ; ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z
A8: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(u 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'or' a) . x = TRUE )
assume A9: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'or' a) . x = TRUE
(u 'or' a) . x = (u . x) 'or' (a . x) by BVFUNC_1:def_4
.= (u . x) 'or' TRUE by A7, A9
.= TRUE by BINARITH:10 ;
hence  (u 'or' a) . x = TRUE ; ::_thesis: verum
end;
 (B_INF (a,(CompF (PA,G)))) . z = TRUE by A7, BVFUNC_1:def_16;
then  (u 'or' (B_INF (a,(CompF (PA,G))))) . z = TRUE by A6, BINARITH:10;
hence  (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z by A8, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA10: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) ) ; ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z
A11: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(u 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'or' a) . x = TRUE )
assume A12: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'or' a) . x = TRUE
(u 'or' a) . x = (u . x) 'or' (a . x) by BVFUNC_1:def_4
.= TRUE 'or' (a . x) by A10, A12
.= TRUE by BINARITH:10 ;
hence  (u 'or' a) . x = TRUE ; ::_thesis: verum
end;
 (u 'or' (B_INF (a,(CompF (PA,G))))) . z = TRUE 'or' ((B_INF (a,(CompF (PA,G)))) . z) by A6, A10, EQREL_1:def_6;
then  (u 'or' (B_INF (a,(CompF (PA,G))))) . z = TRUE by BINARITH:10;
hence  (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z by A11, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA13: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ; ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z
then consider x2 being Element of Y such that
A14: x2 in EqClass (z,(CompF (PA,G))) and
A15: u . x2 <> TRUE ;
consider x1 being Element of Y such that
A16: x1 in EqClass (z,(CompF (PA,G))) and
A17: a . x1 <> TRUE by A13;
 u . x1 = u . x2 by Z, Def8, A16, A14, BVFUNC_1:def_15;
then A18: u . x1 = FALSE by A15, XBOOLEAN:def_3;
A19: (B_INF (a,(CompF (PA,G)))) . z = FALSE by A13, BVFUNC_1:def_16;
 z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
then A20: u . x1 = u . z by Z, Def8, A16, BVFUNC_1:def_15;
 a . x1 = FALSE by A17, XBOOLEAN:def_3;
then  (u 'or' a) . x1 = FALSE 'or' FALSE by A18, BVFUNC_1:def_4;
hence  (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z by A6, A19, A16, A18, A20, BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_2:23
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'or' u),PA,G) = (All (a,PA,G)) 'or' u by Th22;

theorem :: BVFUNC_2:24
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u )
assume Z: u is_independent_of PA,G ; ::_thesis: All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'or' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'or' u) . z = TRUE )
assume A3: (All ((a 'or' u),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE
A4: for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or a . x = TRUE or u . x = TRUE )
proof
let x be Element of Y; ::_thesis: ( not x in EqClass (z,(CompF (PA,G))) or a . x = TRUE or u . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: ( a . x = TRUE or u . x = TRUE )
then  (a 'or' u) . x = TRUE by A3, BVFUNC_1:def_16;
then A5: (a . x) 'or' (u . x) = TRUE by BVFUNC_1:def_4;
 ( u . x = TRUE or u . x = FALSE ) by XBOOLEAN:def_3;
hence  ( a . x = TRUE or u . x = TRUE ) by A5, BINARITH:3; ::_thesis: verum
end;
A6: ((Ex (a,PA,G)) 'or' u) . z = ((Ex (a,PA,G)) . z) 'or' (u . z) by BVFUNC_1:def_4;
percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ;
suppose for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE
then ((Ex (a,PA,G)) 'or' u) . z = ((Ex (a,PA,G)) . z) 'or' TRUE by EQREL_1:def_6, A6
.= TRUE by BINARITH:10 ;
hence  ((Ex (a,PA,G)) 'or' u) . z = TRUE ; ::_thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE
then ((Ex (a,PA,G)) 'or' u) . z = TRUE 'or' (u . z) by A6, BVFUNC_1:def_17
.= TRUE by BINARITH:10 ;
hence  ((Ex (a,PA,G)) 'or' u) . z = TRUE ; ::_thesis: verum
end;
supposeA7: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE
A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
A9: a . z <> TRUE by A7, EQREL_1:def_6;
consider x1 being Element of Y such that
A10: x1 in EqClass (z,(CompF (PA,G))) and
A11: u . x1 <> TRUE by A7;
 u . x1 = u . z by Z, Def8, A8, A10, BVFUNC_1:def_15;
hence  ((Ex (a,PA,G)) 'or' u) . z = TRUE by A4, EQREL_1:def_6, A9, A11; ::_thesis: verum
end;
end;
end;

theorem Th25: :: BVFUNC_2:25
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) )
A1: All ((u '&' a),PA,G) '<' u '&' (All (a,PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u '&' a),PA,G)) . z = TRUE or (u '&' (All (a,PA,G))) . z = TRUE )
assume A2: (All ((u '&' a),PA,G)) . z = TRUE ; ::_thesis: (u '&' (All (a,PA,G))) . z = TRUE
A3: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies u . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: u . x = TRUE
then A4: (u '&' a) . x = TRUE by A2, BVFUNC_1:def_16;
 (u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def_20;
hence  u . x = TRUE by A4, MARGREL1:12; ::_thesis: verum
end;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies a . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: a . x = TRUE
then A5: (u '&' a) . x = TRUE by A2, BVFUNC_1:def_16;
 (u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def_20;
hence  a . x = TRUE by A5, MARGREL1:12; ::_thesis: verum
end;
then A6: ( (u '&' (All (a,PA,G))) . z = (u . z) '&' ((All (a,PA,G)) . z) & (All (a,PA,G)) . z = TRUE ) by BVFUNC_1:def_16, MARGREL1:def_20;
 u . z = TRUE by A3, EQREL_1:def_6;
hence  (u '&' (All (a,PA,G))) . z = TRUE by A6; ::_thesis: verum
end;
assume Z: u is_independent_of PA,G ; ::_thesis: All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
 u '&' (All (a,PA,G)) '<' All ((u '&' a),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u '&' (All (a,PA,G))) . z = TRUE or (All ((u '&' a),PA,G)) . z = TRUE )
A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (u '&' (All (a,PA,G))) . z = TRUE ; ::_thesis: (All ((u '&' a),PA,G)) . z = TRUE
then A9: (u . z) '&' ((All (a,PA,G)) . z) = TRUE by MARGREL1:def_20;
then A10: (All (a,PA,G)) . z = TRUE by MARGREL1:12;
A11: u . z = TRUE by A9, MARGREL1:12;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(u '&' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u '&' a) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u '&' a) . x = TRUE
then  ( a . x = TRUE & u . x = u . z ) by Z, Def8, A10, A8, BVFUNC_1:def_15, BVFUNC_1:def_16;
then (u '&' a) . x = TRUE '&' TRUE by A11, MARGREL1:def_20
.= TRUE ;
hence  (u '&' a) . x = TRUE ; ::_thesis: verum
end;
hence  (All ((u '&' a),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
hence  All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_2:26
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a '&' u),PA,G) = (All (a,PA,G)) '&' u by Th25;

theorem :: BVFUNC_2:27
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u
let G be Subset of (PARTITIONS Y); ::_thesis: for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u
let a, u be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u
let PA be a_partition of Y; ::_thesis: All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a '&' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) '&' u) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume A2: (All ((a '&' u),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE
A3: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
( a . x = TRUE & u . x = TRUE )
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies ( a . x = TRUE & u . x = TRUE ) )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: ( a . x = TRUE & u . x = TRUE )
then  (a '&' u) . x = TRUE by A2, BVFUNC_1:def_16;
then  (a . x) '&' (u . x) = TRUE by MARGREL1:def_20;
hence  ( a . x = TRUE & u . x = TRUE ) by MARGREL1:12; ::_thesis: verum
end;
A4: ((Ex (a,PA,G)) '&' u) . z = ((Ex (a,PA,G)) . z) '&' (u . z) by MARGREL1:def_20;
percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE or ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ;
supposeA5: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE
now__::_thesis:_((Ex_(a,PA,G))_'&'_u)_._z_=_TRUE
percases ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) or for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE
then  (Ex (a,PA,G)) . z = TRUE by BVFUNC_1:def_17;
hence ((Ex (a,PA,G)) '&' u) . z = TRUE '&' TRUE by EQREL_1:def_6, A4, A5
.= TRUE ;
::_thesis: verum
end;
suppose for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE
then  a . z <> TRUE by EQREL_1:def_6;
hence  ((Ex (a,PA,G)) '&' u) . z = TRUE by A3, A1; ::_thesis: verum
end;
end;
end;
hence  ((Ex (a,PA,G)) '&' u) . z = TRUE ; ::_thesis: verum
end;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE
hence  ((Ex (a,PA,G)) '&' u) . z = TRUE by A3; ::_thesis: verum
end;
end;
end;

theorem Th28: :: BVFUNC_2:28
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) )
assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u 'xor' a),PA,G)) . z = TRUE or (u 'xor' (All (a,PA,G))) . z = TRUE )
assume A2: (All ((u 'xor' a),PA,G)) . z = TRUE ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
A4: ( 'not' FALSE = TRUE & (u 'xor' (All (a,PA,G))) . z = ((All (a,PA,G)) . z) 'xor' (u . z) ) by BVFUNC_1:def_5, MARGREL1:11;
percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) or ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ;
suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
then A5: ( u . z = TRUE & a . z = TRUE ) by EQREL_1:def_6;
A6: FALSE '&' TRUE = FALSE by MARGREL1:12;
(u 'xor' a) . z = (a . z) 'xor' (u . z) by BVFUNC_1:def_5
.= FALSE by A5, A6, MARGREL1:11 ;
hence  (u 'xor' (All (a,PA,G))) . z = TRUE by A2, A3, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA7: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A8: x1 in EqClass (z,(CompF (PA,G))) and
 a . x1 <> TRUE ;
A9: u . x1 = TRUE by A7, A8;
A10: (All (a,PA,G)) . z = FALSE by A7, BVFUNC_1:def_16;
 u . z = u . x1 by Z, Def8, A3, A8, BVFUNC_1:def_15;
then (u 'xor' (All (a,PA,G))) . z = TRUE 'or' FALSE by A4, A10, A9
.= TRUE by BINARITH:3 ;
hence  (u 'xor' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A11: x1 in EqClass (z,(CompF (PA,G))) and
A12: u . x1 <> TRUE ;
now__::_thesis:_(u_'xor'_(All_(a,PA,G)))_._z_=_TRUE
percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE or ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ;
supposeA13: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
 u . z = u . x1 by Z, Def8, A3, A11, BVFUNC_1:def_15;
then A14: u . z = FALSE by A12, XBOOLEAN:def_3;
 (All (a,PA,G)) . z = TRUE by A13, BVFUNC_1:def_16;
then (u 'xor' (All (a,PA,G))) . z = FALSE 'or' TRUE by A4, A14
.= TRUE by BINARITH:3 ;
hence  (u 'xor' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE
then consider x2 being Element of Y such that
A15: x2 in EqClass (z,(CompF (PA,G))) and
A16: a . x2 <> TRUE ;
A17: a . x2 = FALSE by A16, XBOOLEAN:def_3;
 u . x1 = u . x2 by Z, Def8, A11, A15, BVFUNC_1:def_15;
then A18: u . x2 = FALSE by A12, XBOOLEAN:def_3;
(u 'xor' a) . x2 = (a . x2) 'xor' (u . x2) by BVFUNC_1:def_5
.= FALSE by A18, A17, MARGREL1:12 ;
hence  (u 'xor' (All (a,PA,G))) . z = TRUE by A2, A15, BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;
hence  (u 'xor' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_2:29
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'xor' u),PA,G) '<' (All (a,PA,G)) 'xor' u by Th28;

theorem Th30: :: BVFUNC_2:30
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) )
A1: 'not' FALSE = TRUE by MARGREL1:11;
assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u 'eqv' a),PA,G)) . z = TRUE or (u 'eqv' (All (a,PA,G))) . z = TRUE )
assume A3: (All ((u 'eqv' a),PA,G)) . z = TRUE ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE
A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ) ;
suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE
then A5: ( (All (a,PA,G)) . z = TRUE & u . z = TRUE ) by EQREL_1:def_6, BVFUNC_1:def_16;
(u 'eqv' (All (a,PA,G))) . z = 'not' ((u . z) 'xor' ((All (a,PA,G)) . z)) by BVFUNC_1:def_9
.= TRUE by A1, A5, MARGREL1:13 ;
hence  (u 'eqv' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
supposeA6: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A7: x1 in EqClass (z,(CompF (PA,G))) and
A8: a . x1 <> TRUE ;
A9: u . x1 = TRUE by A6, A7;
A10: a . x1 = FALSE by A8, XBOOLEAN:def_3;
(u 'eqv' a) . x1 = 'not' ((u . x1) 'xor' (a . x1)) by BVFUNC_1:def_9
.= 'not' (FALSE 'or' TRUE) by A1, A9, A10
.= FALSE by MARGREL1:11, BINARITH:3 ;
hence  (u 'eqv' (All (a,PA,G))) . z = TRUE by A3, A7, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA11: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A12: x1 in EqClass (z,(CompF (PA,G))) and
A13: u . x1 <> TRUE ;
A14: a . x1 = TRUE by A11, A12;
A15: u . x1 = FALSE by A13, XBOOLEAN:def_3;
(u 'eqv' a) . x1 = 'not' ((u . x1) 'xor' (a . x1)) by BVFUNC_1:def_9
.= 'not' (TRUE 'or' FALSE) by A1, A15, A14
.= FALSE by MARGREL1:11, BINARITH:3 ;
hence  (u 'eqv' (All (a,PA,G))) . z = TRUE by A3, A12, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA16: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A17: x1 in EqClass (z,(CompF (PA,G))) and
A18: u . x1 <> TRUE ;
 u . x1 = u . z by Z, Def8, A4, A17, BVFUNC_1:def_15;
then A19: u . z = FALSE by A18, XBOOLEAN:def_3;
A20: (All (a,PA,G)) . z = FALSE by A16, BVFUNC_1:def_16;
(u 'eqv' (All (a,PA,G))) . z = 'not' ((u . z) 'xor' ((All (a,PA,G)) . z)) by BVFUNC_1:def_9
.= TRUE by MARGREL1:11, A20, A19, MARGREL1:13 ;
hence  (u 'eqv' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_2:31
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'eqv' u),PA,G) '<' (All (a,PA,G)) 'eqv' u by Th30;

theorem Th32: :: BVFUNC_2:32
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) )
assume Z: u is_independent_of PA,G ; ::_thesis: Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
A2: Ex ((u 'or' a),PA,G) '<' u 'or' (Ex (a,PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((u 'or' a),PA,G)) . z = TRUE or (u 'or' (Ex (a,PA,G))) . z = TRUE )
A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
A4: (u 'or' (Ex (a,PA,G))) . z = (u . z) 'or' ((Ex (a,PA,G)) . z) by BVFUNC_1:def_4;
assume  (Ex ((u 'or' a),PA,G)) . z = TRUE ; ::_thesis: (u 'or' (Ex (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A5: x1 in EqClass (z,(CompF (PA,G))) and
A6: (u 'or' a) . x1 = TRUE by BVFUNC_1:def_17;
A7: ( u . x1 = TRUE or u . x1 = FALSE ) by XBOOLEAN:def_3;
A8: (u . x1) 'or' (a . x1) = TRUE by A6, BVFUNC_1:def_4;
now__::_thesis:_(_(_u_._x1_=_TRUE_&_(u_'or'_(Ex_(a,PA,G)))_._z_=_TRUE_)_or_(_a_._x1_=_TRUE_&_(u_'or'_(Ex_(a,PA,G)))_._z_=_TRUE_)_)
percases ( u . x1 = TRUE or a . x1 = TRUE ) by A8, A7, BINARITH:3;
caseA9: u . x1 = TRUE ; ::_thesis: (u 'or' (Ex (a,PA,G))) . z = TRUE
 u . z = u . x1 by Z, Def8, A5, A3, BVFUNC_1:def_15;
hence  (u 'or' (Ex (a,PA,G))) . z = TRUE by A4, A9, BINARITH:10; ::_thesis: verum
end;
case a . x1 = TRUE ; ::_thesis: (u 'or' (Ex (a,PA,G))) . z = TRUE
then (u 'or' (Ex (a,PA,G))) . z = (u . z) 'or' TRUE by A5, A4, BVFUNC_1:def_17
.= TRUE by BINARITH:10 ;
hence  (u 'or' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  (u 'or' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
 u 'or' (Ex (a,PA,G)) '<' Ex ((u 'or' a),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'or' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'or' a),PA,G)) . z = TRUE )
A10: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (u 'or' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u 'or' a),PA,G)) . z = TRUE
then A11: (u . z) 'or' ((Ex (a,PA,G)) . z) = TRUE by BVFUNC_1:def_4;
A12: ( (Ex (a,PA,G)) . z = TRUE or (Ex (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_u_._z_=_TRUE_&_(Ex_((u_'or'_a),PA,G))_._z_=_TRUE_)_or_(_(Ex_(a,PA,G))_._z_=_TRUE_&_(Ex_((u_'or'_a),PA,G))_._z_=_TRUE_)_)
percases ( u . z = TRUE or (Ex (a,PA,G)) . z = TRUE ) by A11, A12, BINARITH:3;
case u . z = TRUE ; ::_thesis: (Ex ((u 'or' a),PA,G)) . z = TRUE
then (u 'or' a) . z = TRUE 'or' (a . z) by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
hence  (Ex ((u 'or' a),PA,G)) . z = TRUE by A10, BVFUNC_1:def_17; ::_thesis: verum
end;
case (Ex (a,PA,G)) . z = TRUE ; ::_thesis: (Ex ((u 'or' a),PA,G)) . z = TRUE
then consider x1 being Element of Y such that
A13: x1 in EqClass (z,(CompF (PA,G))) and
A14: a . x1 = TRUE by BVFUNC_1:def_17;
(u 'or' a) . x1 = (u . x1) 'or' (a . x1) by BVFUNC_1:def_4
.= TRUE by A14, BINARITH:10 ;
hence  (Ex ((u 'or' a),PA,G)) . z = TRUE by A13, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((u 'or' a),PA,G)) . z = TRUE ; ::_thesis: verum
end;
hence  Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) by A2, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_2:33
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((a 'or' u),PA,G) = (Ex (a,PA,G)) 'or' u by Th32;

theorem Th34: :: BVFUNC_2:34
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) )
assume Z: u is_independent_of PA,G ; ::_thesis: Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
A2: Ex ((u '&' a),PA,G) '<' u '&' (Ex (a,PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((u '&' a),PA,G)) . z = TRUE or (u '&' (Ex (a,PA,G))) . z = TRUE )
assume  (Ex ((u '&' a),PA,G)) . z = TRUE ; ::_thesis: (u '&' (Ex (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: (u '&' a) . x1 = TRUE by BVFUNC_1:def_17;
A5: (u . x1) '&' (a . x1) = TRUE by A4, MARGREL1:def_20;
then  a . x1 = TRUE by MARGREL1:12;
then A6: (Ex (a,PA,G)) . z = TRUE by A3, BVFUNC_1:def_17;
 z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
then A7: u . z = u . x1 by Z, Def8, A3, BVFUNC_1:def_15;
 u . x1 = TRUE by A5, MARGREL1:12;
then (u '&' (Ex (a,PA,G))) . z = TRUE '&' TRUE by A6, A7, MARGREL1:def_20
.= TRUE ;
hence  (u '&' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: verum
end;
 u '&' (Ex (a,PA,G)) '<' Ex ((u '&' a),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u '&' (Ex (a,PA,G))) . z = TRUE or (Ex ((u '&' a),PA,G)) . z = TRUE )
assume  (u '&' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u '&' a),PA,G)) . z = TRUE
then A8: (u . z) '&' ((Ex (a,PA,G)) . z) = TRUE by MARGREL1:def_20;
then A9: u . z = TRUE by MARGREL1:12;
 (Ex (a,PA,G)) . z = TRUE by A8, MARGREL1:12;
then consider x1 being Element of Y such that
A10: x1 in EqClass (z,(CompF (PA,G))) and
A11: a . x1 = TRUE by BVFUNC_1:def_17;
 z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
then  u . x1 = u . z by Z, Def8, A10, BVFUNC_1:def_15;
then (u '&' a) . x1 = TRUE '&' TRUE by A9, A11, MARGREL1:def_20
.= TRUE ;
hence  (Ex ((u '&' a),PA,G)) . z = TRUE by A10, BVFUNC_1:def_17; ::_thesis: verum
end;
hence  Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) by A2, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_2:35
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((a '&' u),PA,G) = (Ex (a,PA,G)) '&' u by Th34;

theorem :: BVFUNC_2:36
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G)
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G)
let PA be a_partition of Y; ::_thesis: u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'imp' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'imp' a),PA,G)) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (u 'imp' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u 'imp' a),PA,G)) . z = TRUE
then A2: ('not' (u . z)) 'or' ((Ex (a,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
A3: ( (Ex (a,PA,G)) . z = TRUE or (Ex (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(u_._z)_=_TRUE_&_(Ex_((u_'imp'_a),PA,G))_._z_=_TRUE_)_or_(_(Ex_(a,PA,G))_._z_=_TRUE_&_(Ex_((u_'imp'_a),PA,G))_._z_=_TRUE_)_)
percases ( 'not' (u . z) = TRUE or (Ex (a,PA,G)) . z = TRUE ) by A2, A3, BINARITH:3;
caseA4: 'not' (u . z) = TRUE ; ::_thesis: (Ex ((u 'imp' a),PA,G)) . z = TRUE
(u 'imp' a) . z = ('not' (u . z)) 'or' (a . z) by BVFUNC_1:def_8
.= TRUE by A4, BINARITH:10 ;
hence  (Ex ((u 'imp' a),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum
end;
case (Ex (a,PA,G)) . z = TRUE ; ::_thesis: (Ex ((u 'imp' a),PA,G)) . z = TRUE
then consider x1 being Element of Y such that
A5: x1 in EqClass (z,(CompF (PA,G))) and
A6: a . x1 = TRUE by BVFUNC_1:def_17;
(u 'imp' a) . x1 = ('not' (u . x1)) 'or' (a . x1) by BVFUNC_1:def_8
.= TRUE by A6, BINARITH:10 ;
hence  (Ex ((u 'imp' a),PA,G)) . z = TRUE by A5, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_2:37
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let a, u be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' u) . z = TRUE or (Ex ((a 'imp' u),PA,G)) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE
then A2: ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def_8;
A3: ( u . z = TRUE or u . z = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_((Ex_(a,PA,G))_._z)_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_or_(_u_._z_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_)
percases ( 'not' ((Ex (a,PA,G)) . z) = TRUE or u . z = TRUE ) by A2, A3, BINARITH:3;
case 'not' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE
then A4: a . z <> TRUE by A1, BVFUNC_1:def_17, MARGREL1:11;
(a 'imp' u) . z = ('not' (a . z)) 'or' (u . z) by BVFUNC_1:def_8
.= TRUE 'or' (u . z) by MARGREL1:11, A4, XBOOLEAN:def_3
.= TRUE by BINARITH:10 ;
hence  (Ex ((a 'imp' u),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum
end;
caseA5: u . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE
(a 'imp' u) . z = ('not' (a . z)) 'or' (u . z) by BVFUNC_1:def_8
.= TRUE by A5, BINARITH:10 ;
hence  (Ex ((a 'imp' u),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: verum
end;

theorem Th38: :: BVFUNC_2:38
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) )
A1: 'not' FALSE = TRUE by MARGREL1:11;
assume Z: u is_independent_of PA,G ; ::_thesis: u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'xor' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'xor' a),PA,G)) . z = TRUE )
A3: (u 'xor' (Ex (a,PA,G))) . z = (u . z) 'xor' ((Ex (a,PA,G)) . z) by BVFUNC_1:def_5
.= (('not' (u . z)) '&' ((Ex (a,PA,G)) . z)) 'or' ((u . z) '&' ('not' ((Ex (a,PA,G)) . z))) ;
A4: ( (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE or (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = FALSE ) by XBOOLEAN:def_3;
A5: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume A6: (u 'xor' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u 'xor' a),PA,G)) . z = TRUE
now__::_thesis:_(_(_('not'_(u_._z))_'&'_((Ex_(a,PA,G))_._z)_=_TRUE_&_(Ex_((u_'xor'_a),PA,G))_._z_=_TRUE_)_or_(_(u_._z)_'&'_('not'_((Ex_(a,PA,G))_._z))_=_TRUE_&_(Ex_((u_'xor'_a),PA,G))_._z_=_TRUE_)_)
percases ( ('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE or (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE ) by A6, A3, A4, BINARITH:3;
caseA7: ('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((u 'xor' a),PA,G)) . z = TRUE
then  (Ex (a,PA,G)) . z = TRUE by MARGREL1:12;
then consider x1 being Element of Y such that
A8: x1 in EqClass (z,(CompF (PA,G))) and
A9: a . x1 = TRUE by BVFUNC_1:def_17;
A10: u . z = u . x1 by Z, Def8, A5, A8, BVFUNC_1:def_15;
A11: 'not' (u . z) = TRUE by A7, MARGREL1:12;
(u 'xor' a) . x1 = (u . x1) 'xor' (a . x1) by BVFUNC_1:def_5
.= TRUE 'or' FALSE by A11, A9, A10, MARGREL1:11
.= TRUE by BINARITH:10 ;
hence  (Ex ((u 'xor' a),PA,G)) . z = TRUE by A8, BVFUNC_1:def_17; ::_thesis: verum
end;
caseA12: (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE ; ::_thesis: (Ex ((u 'xor' a),PA,G)) . z = TRUE
then  'not' ((Ex (a,PA,G)) . z) = TRUE by MARGREL1:12;
then  a . z <> TRUE by A5, BVFUNC_1:def_17, MARGREL1:11;
then A13: a . z = FALSE by XBOOLEAN:def_3;
A14: u . z = TRUE by A12, MARGREL1:12;
(u 'xor' a) . z = (u . z) 'xor' (a . z) by BVFUNC_1:def_5
.= FALSE 'or' TRUE by A1, A14, A13
.= TRUE by BINARITH:10 ;
hence  (Ex ((u 'xor' a),PA,G)) . z = TRUE by A5, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((u 'xor' a),PA,G)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_2:39
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
(Ex (a,PA,G)) 'xor' u '<' Ex ((a 'xor' u),PA,G) by Th38;