:: BVFUNC_3 semantic presentation

begin


theorem :: BVFUNC_3:1
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 a 'imp' b '<' (All (a,PA,G)) 'imp' (Ex (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 a 'imp' b '<' (All (a,PA,G)) 'imp' (Ex (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 a 'imp' b '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a 'imp' b '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: a 'imp' b '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE )
A1: ( 'not' (a . z) = TRUE or 'not' (a . z) = FALSE ) by XBOOLEAN:def_3;
A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (a 'imp' b) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A1, BINARITH:3;
suppose 'not' (a . z) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  a . z = FALSE by MARGREL1:11;
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by A2, BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' FALSE) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= TRUE 'or' ((Ex (b,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:2
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)) '&' (All (b,PA,G)) '<' a '&' b
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)) '&' (All (b,PA,G)) '<' a '&' b
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)) '&' (All (b,PA,G)) '<' a '&' b
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) '&' (All (b,PA,G)) '<' a '&' b
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) '&' (All (b,PA,G)) '<' a '&' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) '&' (All (b,PA,G))) . z = TRUE or (a '&' b) . z = TRUE )
A1: ((All (a,PA,G)) '&' (All (b,PA,G))) . z = ((All (a,PA,G)) . z) '&' ((All (b,PA,G)) . z) by MARGREL1:def_20;
assume A2: ((All (a,PA,G)) '&' (All (b,PA,G))) . z = TRUE ; ::_thesis: (a '&' b) . z = TRUE
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A2, A1, MARGREL1:12; ::_thesis: verum
end;
A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All (b,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A2, A1, MARGREL1:12; ::_thesis: verum
end;
then A5: b . z = TRUE by A4;
thus (a '&' b) . z = (a . z) '&' (b . z) by MARGREL1:def_20
.= TRUE '&' TRUE by A4, A3, A5
.= TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_3:3
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 a '&' b '<' (Ex (a,PA,G)) '&' (Ex (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 a '&' b '<' (Ex (a,PA,G)) '&' (Ex (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 a '&' b '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a '&' b '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: a '&' b '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a '&' b) . z = TRUE or ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE )
A1: (a '&' b) . z = (a . z) '&' (b . z) by MARGREL1:def_20;
assume A2: (a '&' b) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE
then A3: ( Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))) & a . z = TRUE ) by A1, BVFUNC_2:def_10, MARGREL1:12;
A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
 b . z = TRUE by A2, A1, MARGREL1:12;
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A4, BVFUNC_1:def_17;
then A5: (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
thus ((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 A3, A4, A5, BVFUNC_1:def_17
.= TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_3:4
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 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' 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 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' 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 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))
let PA be a_partition of Y; ::_thesis: 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))
A1: All (b,PA,G) = B_INF (b,(CompF (PA,G))) by BVFUNC_2:def_9;
A2: All (a,PA,G) = B_INF (a,(CompF (PA,G))) by BVFUNC_2:def_9;
A3: (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G)) '<' 'not' ((All (a,PA,G)) '&' (All (b,PA,G)))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE or ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = TRUE )
A4: ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = ((Ex (('not' a),PA,G)) . z) 'or' ((Ex (('not' b),PA,G)) . z) by BVFUNC_1:def_4;
A5: ( (Ex (('not' b),PA,G)) . z = TRUE or (Ex (('not' b),PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
assume A6: ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE ; ::_thesis: ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = TRUE
percases ( (Ex (('not' a),PA,G)) . z = TRUE or (Ex (('not' b),PA,G)) . z = TRUE ) by A6, A4, A5, BINARITH:3;
supposeA7: (Ex (('not' a),PA,G)) . z = TRUE ; ::_thesis: ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_('not'_a)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (('not' a),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A7, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A8: x1 in EqClass (z,(CompF (PA,G))) and
A9: ('not' a) . x1 = TRUE ;
 'not' (a . x1) = TRUE by A9, MARGREL1:def_19;
then A10: a . x1 = FALSE by MARGREL1:11;
thus ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = 'not' (((All (a,PA,G)) '&' (All (b,PA,G))) . z) by MARGREL1:def_19
.= 'not' (((All (a,PA,G)) . z) '&' ((All (b,PA,G)) . z)) by MARGREL1:def_20
.= 'not' (FALSE '&' ((All (b,PA,G)) . z)) by A2, A8, A10, BVFUNC_1:def_16
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ; ::_thesis: verum
end;
supposeA11: (Ex (('not' b),PA,G)) . z = TRUE ; ::_thesis: ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_('not'_b)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not ('not' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (('not' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A11, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A12: x1 in EqClass (z,(CompF (PA,G))) and
A13: ('not' b) . x1 = TRUE ;
 'not' (b . x1) = TRUE by A13, MARGREL1:def_19;
then A14: b . x1 = FALSE by MARGREL1:11;
thus ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = 'not' (((All (a,PA,G)) '&' (All (b,PA,G))) . z) by MARGREL1:def_19
.= 'not' (((All (a,PA,G)) . z) '&' ((All (b,PA,G)) . z)) by MARGREL1:def_20
.= 'not' (((All (a,PA,G)) . z) '&' FALSE) by A1, A12, A14, BVFUNC_1:def_16
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ; ::_thesis: verum
end;
end;
end;
 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) '<' (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = TRUE or ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE )
assume  ('not' ((All (a,PA,G)) '&' (All (b,PA,G)))) . z = TRUE ; ::_thesis: ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE
then A15: 'not' (((All (a,PA,G)) '&' (All (b,PA,G))) . z) = TRUE by MARGREL1:def_19;
 ((All (a,PA,G)) '&' (All (b,PA,G))) . z = ((All (a,PA,G)) . z) '&' ((All (b,PA,G)) . z) by MARGREL1:def_20;
then A16: ((All (a,PA,G)) . z) '&' ((All (b,PA,G)) . z) = FALSE by A15, MARGREL1:11;
percases ( (All (a,PA,G)) . z = FALSE or (All (b,PA,G)) . z = FALSE ) by A16, MARGREL1:12;
suppose (All (a,PA,G)) . z = FALSE ; ::_thesis: ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A17: x1 in EqClass (z,(CompF (PA,G))) and
A18: a . x1 <> TRUE by A2, BVFUNC_1:def_16;
 a . x1 = FALSE by A18, XBOOLEAN:def_3;
then  'not' (a . x1) = TRUE by MARGREL1:11;
then  ('not' a) . x1 = TRUE by MARGREL1:def_19;
then  (B_SUP (('not' a),(CompF (PA,G)))) . z = TRUE by A17, BVFUNC_1:def_17;
then  (Ex (('not' a),PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE 'or' ((Ex (('not' b),PA,G)) . z) by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose (All (b,PA,G)) . z = FALSE ; ::_thesis: ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A19: x1 in EqClass (z,(CompF (PA,G))) and
A20: b . x1 <> TRUE by A1, BVFUNC_1:def_16;
 b . x1 = FALSE by A20, XBOOLEAN:def_3;
then  'not' (b . x1) = TRUE by MARGREL1:11;
then  ('not' b) . x1 = TRUE by MARGREL1:def_19;
then  (B_SUP (('not' b),(CompF (PA,G)))) . z = TRUE by A19, BVFUNC_1:def_17;
then  (Ex (('not' b),PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))) . z = ((Ex (('not' a),PA,G)) . z) 'or' TRUE by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;
hence  'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G)) by A3, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_3:5
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 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' 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 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' 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 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
let PA be a_partition of Y; ::_thesis: 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
A1: All (('not' b),PA,G) = B_INF (('not' b),(CompF (PA,G))) by BVFUNC_2:def_9;
A2: Ex (b,PA,G) = B_SUP (b,(CompF (PA,G))) by BVFUNC_2:def_10;
A3: Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))) by BVFUNC_2:def_10;
A4: (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G)) '<' 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE or ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE )
A5: ( (All (('not' b),PA,G)) . z = TRUE or (All (('not' b),PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
assume  ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE ; ::_thesis: ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE
then A6: ((All (('not' a),PA,G)) . z) 'or' ((All (('not' b),PA,G)) . z) = TRUE by BVFUNC_1:def_4;
percases ( (All (('not' a),PA,G)) . z = TRUE or (All (('not' b),PA,G)) . z = TRUE ) by A6, A5, BINARITH:3;
supposeA7: (All (('not' a),PA,G)) . z = TRUE ; ::_thesis: ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE
A8: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
('not'_a)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (('not' a),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A7, BVFUNC_2:def_9; ::_thesis: verum
end;
A9: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_<>_TRUE
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  ('not' a) . x = TRUE by A8;
then  'not' (a . x) = TRUE by MARGREL1:def_19;
hence  a . x <> TRUE by MARGREL1:11; ::_thesis: verum
end;
thus ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = 'not' (((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z) by MARGREL1:def_19
.= 'not' (((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z)) by MARGREL1:def_20
.= 'not' (FALSE '&' ((Ex (b,PA,G)) . z)) by A3, A9, BVFUNC_1:def_17
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ; ::_thesis: verum
end;
supposeA10: (All (('not' b),PA,G)) . z = TRUE ; ::_thesis: ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE
A11: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
('not'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (('not' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A10, BVFUNC_2:def_9; ::_thesis: verum
end;
A12: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_<>_TRUE
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies b . x <> TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: b . x <> TRUE
then  ('not' b) . x = TRUE by A11;
then  'not' (b . x) = TRUE by MARGREL1:def_19;
hence  b . x <> TRUE by MARGREL1:11; ::_thesis: verum
end;
thus ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = 'not' (((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z) by MARGREL1:def_19
.= 'not' (((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z)) by MARGREL1:def_20
.= 'not' (((Ex (a,PA,G)) . z) '&' FALSE) by A2, A12, BVFUNC_1:def_17
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ; ::_thesis: verum
end;
end;
end;
A13: All (('not' a),PA,G) = B_INF (('not' a),(CompF (PA,G))) by BVFUNC_2:def_9;
 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) '<' (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE or ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE )
assume  ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE ; ::_thesis: ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE
then  'not' (((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z) = TRUE by MARGREL1:def_19;
then  ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = FALSE by MARGREL1:11;
then A14: ((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z) = FALSE by MARGREL1:def_20;
percases ( (Ex (a,PA,G)) . z = FALSE or (Ex (b,PA,G)) . z = FALSE ) by A14, MARGREL1:12;
supposeA15: (Ex (a,PA,G)) . z = FALSE ; ::_thesis: ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE
A16: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
('not'_a)_._x_=_TRUE
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies ('not' a) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: ('not' a) . x = TRUE
then  a . x <> TRUE by A3, A15, BVFUNC_1:def_17;
then  a . x = FALSE by XBOOLEAN:def_3;
then  'not' (a . x) = TRUE by MARGREL1:11;
hence  ('not' a) . x = TRUE by MARGREL1:def_19; ::_thesis: verum
end;
thus ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = ((All (('not' a),PA,G)) . z) 'or' ((All (('not' b),PA,G)) . z) by BVFUNC_1:def_4
.= TRUE 'or' ((All (('not' b),PA,G)) . z) by A13, A16, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
supposeA17: (Ex (b,PA,G)) . z = FALSE ; ::_thesis: ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE
A18: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
('not'_b)_._x_=_TRUE
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies ('not' b) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: ('not' b) . x = TRUE
then  b . x <> TRUE by A2, A17, BVFUNC_1:def_17;
then  b . x = FALSE by XBOOLEAN:def_3;
then  'not' (b . x) = TRUE by MARGREL1:11;
hence  ('not' b) . x = TRUE by MARGREL1:def_19; ::_thesis: verum
end;
thus ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = ((All (('not' a),PA,G)) . z) 'or' ((All (('not' b),PA,G)) . z) by BVFUNC_1:def_4
.= ((All (('not' a),PA,G)) . z) 'or' TRUE by A1, A18, BVFUNC_1:def_16
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
end;
end;
hence  'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G)) by A4, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_3:6
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)) '<' a 'or' b
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)) '<' a 'or' b
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)) '<' a 'or' b
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)) '<' a 'or' b
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b
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 (a 'or' b) . z = TRUE )
A1: ( (All (a,PA,G)) . z = TRUE or (All (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3;
A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE ; ::_thesis: (a 'or' b) . z = TRUE
then A3: ((All (a,PA,G)) . z) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def_4;
percases ( (All (a,PA,G)) . z = TRUE or (All (b,PA,G)) . z = TRUE ) by A3, A1, BINARITH:3;
supposeA4: (All (a,PA,G)) . z = TRUE ; ::_thesis: (a 'or' b) . z = TRUE
A5: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A4, BVFUNC_2:def_9; ::_thesis: verum
end;
thus (a 'or' b) . z = (a . z) 'or' (b . z) by BVFUNC_1:def_4
.= TRUE 'or' (b . z) by A2, A5
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
supposeA6: (All (b,PA,G)) . z = TRUE ; ::_thesis: (a 'or' b) . z = TRUE
A7: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A6, BVFUNC_2:def_9; ::_thesis: verum
end;
thus (a 'or' b) . z = (a . z) 'or' (b . z) by BVFUNC_1:def_4
.= (a . z) 'or' TRUE by A2, A7
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:7
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 a 'or' b '<' (Ex (a,PA,G)) 'or' (Ex (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 a 'or' b '<' (Ex (a,PA,G)) 'or' (Ex (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 a 'or' b '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a 'or' b '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: a 'or' b '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
A1: Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))) by BVFUNC_2:def_10;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'or' b) . z = TRUE or ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE )
A2: Ex (b,PA,G) = B_SUP (b,(CompF (PA,G))) by BVFUNC_2:def_10;
A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (a 'or' b) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then A4: (a . z) 'or' (b . z) = TRUE by BVFUNC_1:def_4;
A5: ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
percases ( a . z = TRUE or b . z = TRUE ) by A4, A5, BINARITH:3;
supposeA6: a . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
thus ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_4
.= TRUE 'or' ((Ex (b,PA,G)) . z) by A1, A3, A6, BVFUNC_1:def_17
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
supposeA7: b . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
thus ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_4
.= ((Ex (a,PA,G)) . z) 'or' TRUE by A2, A3, A7, BVFUNC_1:def_17
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:8
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 a 'xor' b '<' ('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' 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 a 'xor' b '<' ('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' 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 a 'xor' b '<' ('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a 'xor' b '<' ('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))
let PA be a_partition of Y; ::_thesis: a 'xor' b '<' ('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))
A1: Ex (('not' a),PA,G) = B_SUP (('not' a),(CompF (PA,G))) by BVFUNC_2:def_10;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'xor' b) . z = TRUE or (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))) . z = TRUE )
A2: Ex (('not' b),PA,G) = B_SUP (('not' b),(CompF (PA,G))) by BVFUNC_2:def_10;
A3: ( (a . z) '&' ('not' (b . z)) = TRUE or (a . z) '&' ('not' (b . z)) = FALSE ) by XBOOLEAN:def_3;
A4: (a 'xor' b) . z = (a . z) 'xor' (b . z) by BVFUNC_1:def_5
.= (('not' (a . z)) '&' (b . z)) 'or' ((a . z) '&' ('not' (b . z))) ;
A5: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
A6: FALSE '&' TRUE = FALSE by MARGREL1:13;
assume A7: (a 'xor' b) . z = TRUE ; ::_thesis: (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))) . z = TRUE
percases ( ('not' (a . z)) '&' (b . z) = TRUE or (a . z) '&' ('not' (b . z)) = TRUE ) by A7, A4, A3, BINARITH:3;
supposeA8: ('not' (a . z)) '&' (b . z) = TRUE ; ::_thesis: (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))) . z = TRUE
then  'not' (a . z) = TRUE by MARGREL1:12;
then  ('not' a) . z = TRUE by MARGREL1:def_19;
then A9: (B_SUP (('not' a),(CompF (PA,G)))) . z = TRUE by A5, BVFUNC_1:def_17;
A10: ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G)))) . z = 'not' (((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))) . z) by MARGREL1:def_19;
 b . z = TRUE by A8, MARGREL1:12;
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A5, BVFUNC_1:def_17;
then A11: (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
A12: ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G))) . z = ((Ex (('not' a),PA,G)) . z) 'xor' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_5
.= FALSE by A1, A6, A9, A11, MARGREL1:11 ;
thus (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))) . z = (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) . z) 'or' (('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G)))) . z) by BVFUNC_1:def_4
.= ('not' FALSE) 'or' ('not' (((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))) . z)) by A12, A10, MARGREL1:def_19
.= TRUE 'or' ('not' (((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))) . z)) by MARGREL1:11
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
supposeA13: (a . z) '&' ('not' (b . z)) = TRUE ; ::_thesis: (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))) . z = TRUE
then  a . z = TRUE by MARGREL1:12;
then  (B_SUP (a,(CompF (PA,G)))) . z = TRUE by A5, BVFUNC_1:def_17;
then A14: (Ex (a,PA,G)) . z = TRUE by BVFUNC_2:def_10;
A15: ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G)))) . z = 'not' (((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))) . z) by MARGREL1:def_19;
 'not' (b . z) = TRUE by A13, MARGREL1:12;
then  ('not' b) . z = TRUE by MARGREL1:def_19;
then A16: (B_SUP (('not' b),(CompF (PA,G)))) . z = TRUE by A5, BVFUNC_1:def_17;
A17: ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))) . z = ((Ex (a,PA,G)) . z) 'xor' ((Ex (('not' b),PA,G)) . z) by BVFUNC_1:def_5
.= FALSE by A2, A6, A16, A14, MARGREL1:11 ;
thus (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))) . z = (('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) . z) 'or' (('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G)))) . z) by BVFUNC_1:def_4
.= ('not' (((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G))) . z)) 'or' ('not' FALSE) by A17, A15, MARGREL1:def_19
.= ('not' (((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G))) . z)) 'or' TRUE by MARGREL1:11
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:9
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 'or' b),PA,G) '<' (All (a,PA,G)) 'or' (Ex (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 'or' b),PA,G) '<' (All (a,PA,G)) 'or' (Ex (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 'or' b),PA,G) '<' (All (a,PA,G)) 'or' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a 'or' b),PA,G) '<' (All (a,PA,G)) 'or' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'or' b),PA,G) '<' (All (a,PA,G)) 'or' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'or' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE )
assume A1: (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'or'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'or' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'or' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A1, BVFUNC_2:def_9; ::_thesis: verum
end;
percases ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & b . 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 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 holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ) ;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ; ::_thesis: ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = ((All (a,PA,G)) . z) 'or' TRUE by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
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 holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ; ::_thesis: ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then  (B_INF (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = TRUE by BVFUNC_2:def_9;
hence ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA3: ( 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 b . x = TRUE ) ) ) ; ::_thesis: ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: a . x1 <> TRUE ;
A6: b . x1 <> TRUE by A3, A4;
A7: a . x1 = FALSE by A5, XBOOLEAN:def_3;
(a 'or' b) . x1 = (a . x1) 'or' (b . x1) by BVFUNC_1:def_4
.= FALSE 'or' FALSE by A6, A7, XBOOLEAN:def_3
.= FALSE ;
hence  ((All (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE by A2, A4; ::_thesis: verum
end;
end;
end;

Lm1: now__::_thesis:_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
for_z_being_Element_of_Y_st_(All_((a_'or'_b),PA,G))_._z_=_TRUE_holds_
for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'or'_b)_._x_=_TRUE
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
for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y
for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let PA be a_partition of Y; ::_thesis: for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let z be Element of Y; ::_thesis: ( (All ((a 'or' b),PA,G)) . z = TRUE implies for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE )
assume A1: (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'or' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'or' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A1, BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:10
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 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (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 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (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 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (All (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (All (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (All (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'or' b),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE )
assume A1: (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (All (b,PA,G))) . 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 st x in EqClass (z,(CompF (PA,G))) holds
b . 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 b . x = TRUE ) & ( 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)) 'or' (All (b,PA,G))) . z = TRUE
then  (B_SUP (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE 'or' ((All (b,PA,G)) . z) by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . 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' (All (b,PA,G))) . z = TRUE
then  (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
then  (All (b,PA,G)) . z = TRUE by BVFUNC_2:def_9;
hence ((Ex (a,PA,G)) 'or' (All (b,PA,G))) . z = ((Ex (a,PA,G)) . z) 'or' TRUE by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA2: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . 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' (All (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: b . x1 <> TRUE ;
A5: a . x1 <> TRUE by A2, A3;
A6: b . x1 = FALSE by A4, XBOOLEAN:def_3;
(a 'or' b) . x1 = (a . x1) 'or' (b . x1) by BVFUNC_1:def_4
.= FALSE 'or' FALSE by A5, A6, XBOOLEAN:def_3
.= FALSE ;
hence  ((Ex (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE by A1, A3, Lm1; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:11
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 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (Ex (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 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (Ex (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 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'or' b),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then  (a 'or' b) . z = TRUE by A1, Lm1;
then A2: (a . z) 'or' (b . z) = TRUE by BVFUNC_1:def_4;
A3: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
percases ( a . z = TRUE or b . z = TRUE ) by A2, A3, BINARITH:3;
suppose a . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (a,(CompF (PA,G)))) . z = TRUE by A1, BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A1, BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (a,PA,G)) 'or' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) 'or' TRUE by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:12
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)) '&' (All (b,PA,G)) '<' Ex ((a '&' 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)) '&' (All (b,PA,G)) '<' Ex ((a '&' 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)) '&' (All (b,PA,G)) '<' Ex ((a '&' b),PA,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) '&' (All (b,PA,G)) '<' Ex ((a '&' b),PA,G)
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) '&' (All (b,PA,G)) '<' Ex ((a '&' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) '&' (All (b,PA,G))) . z = TRUE or (Ex ((a '&' b),PA,G)) . z = TRUE )
assume  ((Ex (a,PA,G)) '&' (All (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then A1: ((Ex (a,PA,G)) . z) '&' ((All (b,PA,G)) . z) = TRUE by MARGREL1:def_20;
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All (b,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_a_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: a . x1 = TRUE ;
(a '&' b) . x1 = (a . x1) '&' (b . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A3, A4, A2
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A3, BVFUNC_1:def_17;
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;

theorem :: BVFUNC_3: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)) '&' (Ex (b,PA,G)) '<' Ex ((a '&' 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)) '&' (Ex (b,PA,G)) '<' Ex ((a '&' 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)) '&' (Ex (b,PA,G)) '<' Ex ((a '&' b),PA,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) '&' (Ex (b,PA,G)) '<' Ex ((a '&' b),PA,G)
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) '&' (Ex (b,PA,G)) '<' Ex ((a '&' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE or (Ex ((a '&' b),PA,G)) . z = TRUE )
assume  ((All (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then A1: ((All (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z) = TRUE by MARGREL1:def_20;
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_b_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: b . x1 = TRUE ;
(a '&' b) . x1 = (a . x1) '&' (b . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A3, A4, A2
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A3, BVFUNC_1:def_17;
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;

Lm2: now__::_thesis:_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
for_z_being_Element_of_Y_st_(All_((a_'imp'_b),PA,G))_._z_=_TRUE_holds_
for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_b)_._x_=_TRUE
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
for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y
for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let PA be a_partition of Y; ::_thesis: for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let z be Element of Y; ::_thesis: ( (All ((a 'imp' b),PA,G)) . z = TRUE implies for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE )
assume A1: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A1, BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3: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' (Ex (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' (Ex (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' (Ex (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' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
A1: All (a,PA,G) = B_INF (a,(CompF (PA,G))) by BVFUNC_2:def_9;
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' (Ex (b,PA,G))) . z = TRUE )
assume A2: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
percases ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & b . 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 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 holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ) ;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
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 holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then A4: ( b . z <> TRUE & a . z = TRUE ) by A3;
(a 'imp' b) . z = ('not' (a . z)) 'or' (b . z) by BVFUNC_1:def_8
.= ('not' TRUE) 'or' FALSE by A4, XBOOLEAN:def_3
.= FALSE 'or' FALSE by MARGREL1:11
.= FALSE ;
hence  ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE by A2, A3, Lm2; ::_thesis: verum
end;
supposeA5: ( 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 b . x = TRUE ) ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
thus ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= ('not' FALSE) 'or' ((Ex (b,PA,G)) . z) by A1, A5, BVFUNC_1:def_16
.= TRUE 'or' ((Ex (b,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:15
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) '<' (Ex (a,PA,G)) 'imp' (Ex (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) '<' (Ex (a,PA,G)) 'imp' (Ex (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) '<' (Ex (a,PA,G)) 'imp' (Ex (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) '<' (Ex (a,PA,G)) 'imp' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'imp' b),PA,G) '<' (Ex (a,PA,G)) 'imp' (Ex (b,PA,G))
A1: Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))) by BVFUNC_2:def_10;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'imp' b),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE )
assume A2: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
percases ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) or ( ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ) ;
suppose ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA3: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: a . x1 = TRUE ;
A6: b . 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  ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE by A2, A4, Lm2; ::_thesis: verum
end;
supposeA7: ( ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
thus ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= ('not' FALSE) 'or' ((Ex (b,PA,G)) . z) by A1, A7, BVFUNC_1:def_17
.= TRUE 'or' ((Ex (b,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3: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)) 'imp' (All (b,PA,G)) '<' All ((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' (All (b,PA,G)) '<' All ((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' (All (b,PA,G)) '<' All ((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' (All (b,PA,G)) '<' All ((a 'imp' b),PA,G)
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'imp' (All (b,PA,G)) '<' All ((a 'imp' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE or (All ((a 'imp' b),PA,G)) . z = TRUE )
assume  ((Ex (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: (All ((a 'imp' b),PA,G)) . z = TRUE
then A1: ('not' ((Ex (a,PA,G)) . z)) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
percases ( 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))) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) or ( ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ) ;
supposeA2: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ; ::_thesis: (All ((a 'imp' b),PA,G)) . z = TRUE
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' b) . x = TRUE )
assume A3: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' b) . x = TRUE
thus (a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' TRUE by A2, A3
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' b),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;
supposeA4: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: (All ((a 'imp' b),PA,G)) . z = TRUE
then  (B_SUP (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = TRUE by BVFUNC_2:def_10;
then A5: 'not' ((Ex (a,PA,G)) . z) = FALSE by MARGREL1:11;
 (B_INF (b,(CompF (PA,G)))) . z = FALSE by A4, BVFUNC_1:def_16;
then  (All (b,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  (All ((a 'imp' b),PA,G)) . z = TRUE by A1, A5; ::_thesis: verum
end;
supposeA6: ( ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or 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 'imp' b),PA,G)) . z = TRUE
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_b)_._x_=_TRUE
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' b) . x = TRUE )
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' b) . x = TRUE
then A7: a . x <> TRUE by A6;
thus (a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) by BVFUNC_1:def_8
.= ('not' FALSE) 'or' (b . x) by A7, XBOOLEAN:def_3
.= TRUE 'or' (b . x) by MARGREL1:11
.= TRUE by BINARITH:10 ; ::_thesis: verum
end;
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' b),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3: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 a 'imp' b '<' a 'imp' (Ex (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 a 'imp' b '<' a 'imp' (Ex (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 a 'imp' b '<' a 'imp' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a 'imp' b '<' a 'imp' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: a 'imp' b '<' a 'imp' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or (a 'imp' (Ex (b,PA,G))) . z = TRUE )
A1: ( 'not' (a . z) = TRUE or 'not' (a . z) = FALSE ) by XBOOLEAN:def_3;
A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (a 'imp' b) . z = TRUE ; ::_thesis: (a 'imp' (Ex (b,PA,G))) . z = TRUE
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A1, BINARITH:3;
suppose 'not' (a . z) = TRUE ; ::_thesis: (a 'imp' (Ex (b,PA,G))) . z = TRUE
hence (a 'imp' (Ex (b,PA,G))) . z = TRUE 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . z = TRUE ; ::_thesis: (a 'imp' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence (a 'imp' (Ex (b,PA,G))) . z = ('not' (a . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:18
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 a 'imp' b '<' (All (a,PA,G)) 'imp' b
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 a 'imp' b '<' (All (a,PA,G)) 'imp' b
let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a 'imp' b '<' (All (a,PA,G)) 'imp' b
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a 'imp' b '<' (All (a,PA,G)) 'imp' b
let PA be a_partition of Y; ::_thesis: a 'imp' b '<' (All (a,PA,G)) 'imp' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or ((All (a,PA,G)) 'imp' b) . z = TRUE )
A1: ( 'not' (a . z) = TRUE or 'not' (a . z) = FALSE ) by XBOOLEAN:def_3;
A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  (a 'imp' b) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' b) . z = TRUE
then A3: ('not' (a . z)) 'or' (b . z) = TRUE by BVFUNC_1:def_8;
percases ( 'not' (a . z) = TRUE or b . z = TRUE ) by A3, A1, BINARITH:3;
suppose 'not' (a . z) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' b) . z = TRUE
then  a . z = FALSE by MARGREL1:11;
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by A2, BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence ((All (a,PA,G)) 'imp' b) . z = ('not' FALSE) 'or' (b . z) by BVFUNC_1:def_8
.= TRUE 'or' (b . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' b) . z = TRUE
hence ((All (a,PA,G)) 'imp' b) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:19
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 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (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 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (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 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: Ex ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((a 'imp' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE )
assume A1: (Ex ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'imp'_b)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (a 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A1, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A2: x1 in EqClass (z,(CompF (PA,G))) and
A3: (a 'imp' b) . x1 = TRUE ;
A4: ('not' (a . x1)) 'or' (b . x1) = TRUE by A3, BVFUNC_1:def_8;
A5: ( b . x1 = TRUE or b . x1 = FALSE ) by XBOOLEAN:def_3;
percases ( 'not' (a . x1) = TRUE or b . x1 = TRUE ) by A4, A5, BINARITH:3;
suppose 'not' (a . x1) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  a . x1 = FALSE by MARGREL1:11;
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by A2, BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' FALSE) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= TRUE 'or' ((Ex (b,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . x1 = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:20
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) '<' (Ex (b,PA,G)) 'imp' (Ex ((a '&' 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) '<' (Ex (b,PA,G)) 'imp' (Ex ((a '&' 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) '<' (Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All (a,PA,G) '<' (Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))
let PA be a_partition of Y; ::_thesis: All (a,PA,G) '<' (Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (a,PA,G)) . z = TRUE or ((Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))) . z = TRUE )
assume A1: (All (a,PA,G)) . z = TRUE ; ::_thesis: ((Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))) . z = TRUE
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A1, BVFUNC_2:def_9; ::_thesis: verum
end;
percases ( (Ex (b,PA,G)) . z = TRUE or (Ex (b,PA,G)) . z <> TRUE ) ;
supposeA3: (Ex (b,PA,G)) . z = TRUE ; ::_thesis: ((Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_b_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A3, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: b . x1 = TRUE ;
(a '&' b) . x1 = (a . x1) '&' (b . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A2, A4, A5
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A4, BVFUNC_1:def_17;
then  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))) . z = ('not' ((Ex (b,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose (Ex (b,PA,G)) . z <> TRUE ; ::_thesis: ((Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))) . z = TRUE
then  (Ex (b,PA,G)) . z = FALSE by XBOOLEAN:def_3;
hence ((Ex (b,PA,G)) 'imp' (Ex ((a '&' b),PA,G))) . z = ('not' FALSE) 'or' ((Ex ((a '&' b),PA,G)) . z) by BVFUNC_1:def_8
.= TRUE 'or' ((Ex ((a '&' b),PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3: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
Ex ((u 'imp' a),PA,G) '<' u 'imp' (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 'imp' a),PA,G) '<' u 'imp' (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 'imp' a),PA,G) '<' u 'imp' (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 'imp' a),PA,G) '<' u 'imp' (Ex (a,PA,G))
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex ((u 'imp' a),PA,G) '<' u 'imp' (Ex (a,PA,G)) )
assume  u is_independent_of PA,G ; ::_thesis: Ex ((u 'imp' a),PA,G) '<' u 'imp' (Ex (a,PA,G))
then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((u 'imp' a),PA,G)) . z = TRUE or (u 'imp' (Ex (a,PA,G))) . z = TRUE )
A2: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6;
assume A3: (Ex ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: (u 'imp' (Ex (a,PA,G))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(u_'imp'_a)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (u 'imp' a) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((u 'imp' a),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A3, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: (u 'imp' a) . x1 = TRUE ;
A6: ('not' (u . x1)) 'or' (a . x1) = TRUE by A5, BVFUNC_1:def_8;
A7: ( 'not' (u . x1) = TRUE or 'not' (u . x1) = FALSE ) by XBOOLEAN:def_3;
percases ( 'not' (u . x1) = TRUE or a . x1 = TRUE ) by A6, A7, BINARITH:3;
supposeA8: 'not' (u . x1) = TRUE ; ::_thesis: (u 'imp' (Ex (a,PA,G))) . z = TRUE
 u . x1 = u . z by A1, A4, A2, BVFUNC_1:def_15;
then  u . z = FALSE by A8, MARGREL1:11;
hence (u 'imp' (Ex (a,PA,G))) . z = ('not' FALSE) 'or' ((Ex (a,PA,G)) . z) by BVFUNC_1:def_8
.= TRUE 'or' ((Ex (a,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose a . x1 = TRUE ; ::_thesis: (u 'imp' (Ex (a,PA,G))) . z = TRUE
then  (B_SUP (a,(CompF (PA,G)))) . z = TRUE by A4, BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence (u 'imp' (Ex (a,PA,G))) . z = ('not' (u . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3: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
Ex ((a 'imp' u),PA,G) '<' (All (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
Ex ((a 'imp' u),PA,G) '<' (All (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
Ex ((a 'imp' u),PA,G) '<' (All (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
Ex ((a 'imp' u),PA,G) '<' (All (a,PA,G)) 'imp' u
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex ((a 'imp' u),PA,G) '<' (All (a,PA,G)) 'imp' u )
assume  u is_independent_of PA,G ; ::_thesis: Ex ((a 'imp' u),PA,G) '<' (All (a,PA,G)) 'imp' u
then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((a 'imp' u),PA,G)) . z = TRUE or ((All (a,PA,G)) 'imp' u) . z = TRUE )
A2: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6;
assume A3: (Ex ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'imp'_u)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (a 'imp' u) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((a 'imp' u),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A3, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: (a 'imp' u) . x1 = TRUE ;
A6: ('not' (a . x1)) 'or' (u . x1) = TRUE by A5, BVFUNC_1:def_8;
A7: ( 'not' (a . x1) = TRUE or 'not' (a . x1) = FALSE ) by XBOOLEAN:def_3;
percases ( 'not' (a . x1) = TRUE or u . x1 = TRUE ) by A6, A7, BINARITH:3;
suppose 'not' (a . x1) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . z = TRUE
then  a . x1 = FALSE by MARGREL1:11;
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by A4, BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence ((All (a,PA,G)) 'imp' u) . z = ('not' FALSE) 'or' (u . z) by BVFUNC_1:def_8
.= TRUE 'or' (u . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA8: u . x1 = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . z = TRUE
 u . x1 = u . z by A1, A4, A2, BVFUNC_1:def_15;
hence ((All (a,PA,G)) 'imp' u) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by A8, BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:23
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)) '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 (All (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 (All (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 (All (a,PA,G)) 'imp' (Ex (b,PA,G)) = Ex ((a 'imp' b),PA,G)
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'imp' (Ex (b,PA,G)) = Ex ((a 'imp' b),PA,G)
A1: All (a,PA,G) = B_INF (a,(CompF (PA,G))) by BVFUNC_2:def_9;
A2: (All (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE or (Ex ((a 'imp' b),PA,G)) . z = TRUE )
A3: ( 'not' ((All (a,PA,G)) . z) = TRUE or 'not' ((All (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
assume  ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE
then A4: ('not' ((All (a,PA,G)) . z)) 'or' ((Ex (b,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
percases ( 'not' ((All (a,PA,G)) . z) = TRUE or (Ex (b,PA,G)) . z = TRUE ) by A4, A3, BINARITH:3;
suppose 'not' ((All (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE
then  (All (a,PA,G)) . z = FALSE by MARGREL1:11;
then consider x1 being Element of Y such that
A5: x1 in EqClass (z,(CompF (PA,G))) and
A6: a . x1 <> TRUE by A1, BVFUNC_1:def_16;
(a 'imp' b) . x1 = ('not' (a . x1)) 'or' (b . x1) by BVFUNC_1:def_8
.= ('not' FALSE) 'or' (b . x1) by A6, XBOOLEAN:def_3
.= TRUE 'or' (b . x1) by MARGREL1:11
.= TRUE by BINARITH:10 ;
then  (B_SUP ((a 'imp' b),(CompF (PA,G)))) . z = TRUE by A5, BVFUNC_1:def_17;
hence  (Ex ((a 'imp' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
supposeA7: (Ex (b,PA,G)) . z = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_b_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A7, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A8: x1 in EqClass (z,(CompF (PA,G))) and
A9: b . x1 = TRUE ;
(a 'imp' b) . x1 = ('not' (a . x1)) 'or' TRUE by A9, BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
then  (B_SUP ((a 'imp' b),(CompF (PA,G)))) . z = TRUE by A8, BVFUNC_1:def_17;
hence  (Ex ((a 'imp' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
end;
end;
 Ex ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((a 'imp' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE )
assume A10: (Ex ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'imp'_b)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (a 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A10, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A11: x1 in EqClass (z,(CompF (PA,G))) and
A12: (a 'imp' b) . x1 = TRUE ;
A13: ('not' (a . x1)) 'or' (b . x1) = TRUE by A12, BVFUNC_1:def_8;
A14: ( 'not' (a . x1) = TRUE or 'not' (a . x1) = FALSE ) by XBOOLEAN:def_3;
percases ( 'not' (a . x1) = TRUE or b . x1 = TRUE ) by A13, A14, BINARITH:3;
suppose 'not' (a . x1) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  a . x1 = FALSE by MARGREL1:11;
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by A11, BVFUNC_1:def_16;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' FALSE) 'or' ((Ex (b,PA,G)) . z) by A1, BVFUNC_1:def_8
.= TRUE 'or' ((Ex (b,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . x1 = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A11, BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;
hence  (All (a,PA,G)) 'imp' (Ex (b,PA,G)) = Ex ((a 'imp' b),PA,G) by A2, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_3:24
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)) 'imp' (All (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (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)) 'imp' (All (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (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)) 'imp' (All (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'imp' (All (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'imp' (All (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE or ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE )
A1: ( 'not' ((All (a,PA,G)) . z) = TRUE or 'not' ((All (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
A2: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then A3: ('not' ((All (a,PA,G)) . z)) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
percases ( 'not' ((All (a,PA,G)) . z) = TRUE or (All (b,PA,G)) . z = TRUE ) by A3, A1, BINARITH:3;
suppose 'not' ((All (a,PA,G)) . z) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA4: (All (b,PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A4, BVFUNC_2:def_9; ::_thesis: verum
end;
then  b . z = TRUE by A2;
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = TRUE by BVFUNC_2:def_10;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:25
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)) '<' (All (a,PA,G)) 'imp' (Ex (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)) '<' (All (a,PA,G)) 'imp' (Ex (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)) '<' (All (a,PA,G)) 'imp' (Ex (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)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
A1: Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))) by BVFUNC_2:def_10;
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 ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE )
A2: ( 'not' ((Ex (a,PA,G)) . z) = TRUE or 'not' ((Ex (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
assume  ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then A3: ('not' ((Ex (a,PA,G)) . z)) 'or' ((Ex (b,PA,G)) . z) = TRUE by BVFUNC_1:def_8;
A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
percases ( 'not' ((Ex (a,PA,G)) . z) = TRUE or (Ex (b,PA,G)) . z = TRUE ) by A3, A2, BINARITH:3;
suppose 'not' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
then  (Ex (a,PA,G)) . z = FALSE by MARGREL1:11;
then  a . z <> TRUE by A1, A4, BVFUNC_1:def_17;
then  (B_INF (a,(CompF (PA,G)))) . z = FALSE by A4, BVFUNC_1:def_16;
then  (All (a,PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' FALSE) 'or' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_8
.= TRUE 'or' ((Ex (b,PA,G)) . z) by MARGREL1:11
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose (Ex (b,PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE
hence ((All (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;

theorem Th26: :: BVFUNC_3:26
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 ((('not' 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 'imp' b),PA,G) = All ((('not' 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 'imp' b),PA,G) = All ((('not' a) 'or' 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 ((('not' a) 'or' b),PA,G)
let PA be a_partition of Y; ::_thesis: All ((a 'imp' b),PA,G) = All ((('not' a) 'or' b),PA,G)
A1: All ((('not' a) 'or' b),PA,G) '<' All ((a 'imp' b),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((('not' a) 'or' b),PA,G)) . z = TRUE or (All ((a 'imp' b),PA,G)) . z = TRUE )
assume A2: (All ((('not' a) 'or' b),PA,G)) . z = TRUE ; ::_thesis: (All ((a 'imp' b),PA,G)) . z = TRUE
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(('not'_a)_'or'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (('not' a) 'or' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((('not' a) 'or' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A2, BVFUNC_2:def_9; ::_thesis: verum
end;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' b) . x = TRUE )
A4: ( ('not' a) . x = TRUE or ('not' a) . x = FALSE ) by XBOOLEAN:def_3;
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' b) . x = TRUE
then  (('not' a) 'or' b) . x = TRUE by A3;
then A5: (('not' a) . x) 'or' (b . x) = TRUE by BVFUNC_1:def_4;
percases ( ('not' a) . x = TRUE or b . x = TRUE ) by A5, A4, BINARITH:3;
suppose ('not' a) . x = TRUE ; ::_thesis: (a 'imp' b) . x = TRUE
then  'not' (a . x) = TRUE by MARGREL1:def_19;
hence (a 'imp' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . x = TRUE ; ::_thesis: (a 'imp' b) . x = TRUE
hence (a 'imp' b) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' b),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;
 All ((a 'imp' b),PA,G) '<' All ((('not' a) 'or' b),PA,G)
proof
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'imp' b),PA,G)) . z = TRUE or (All ((('not' a) 'or' b),PA,G)) . z = TRUE )
assume A6: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: (All ((('not' a) 'or' b),PA,G)) . z = TRUE
A7: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A6, BVFUNC_2:def_9; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(('not'_a)_'or'_b)_._x_=_TRUE
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (('not' a) 'or' b) . b1 = TRUE )
A8: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3;
assume  x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (('not' a) 'or' b) . b1 = TRUE
then  (a 'imp' b) . x = TRUE by A7;
then A9: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
percases ( 'not' (a . x) = TRUE or b . x = TRUE ) by A9, A8, BINARITH:3;
suppose 'not' (a . x) = TRUE ; ::_thesis: (('not' a) 'or' b) . b1 = TRUE
then  ('not' a) . x = TRUE by MARGREL1:def_19;
hence (('not' a) 'or' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose b . x = TRUE ; ::_thesis: (('not' a) 'or' b) . b1 = TRUE
hence (('not' a) 'or' b) . x = (('not' a) . x) 'or' TRUE by BVFUNC_1:def_4
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;
then  (B_INF ((('not' a) 'or' b),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((('not' a) 'or' b),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;
hence  All ((a 'imp' b),PA,G) = All ((('not' a) 'or' b),PA,G) by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_3:27
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) = 'not' (Ex ((a '&' ('not' 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) = 'not' (Ex ((a '&' ('not' 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) = 'not' (Ex ((a '&' ('not' 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) = 'not' (Ex ((a '&' ('not' b)),PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'imp' b),PA,G) = 'not' (Ex ((a '&' ('not' b)),PA,G))
 ( 'not' (All ((('not' a) 'or' b),PA,G)) = Ex (('not' (('not' a) 'or' b)),PA,G) & 'not' (('not' a) 'or' b) = ('not' ('not' a)) '&' ('not' b) ) by BVFUNC_1:13, BVFUNC_2:18;
hence  All ((a 'imp' b),PA,G) = 'not' (Ex ((a '&' ('not' b)),PA,G)) by Th26; ::_thesis: verum
end;

theorem :: BVFUNC_3:28
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) '<' 'not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' 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) '<' 'not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' 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) '<' 'not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex (a,PA,G) '<' 'not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))
let PA be a_partition of Y; ::_thesis: Ex (a,PA,G) '<' 'not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex (a,PA,G)) . z = TRUE or ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = TRUE )
A1: ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = 'not' (((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G))) . z) by MARGREL1:def_19
.= 'not' (((All ((a 'imp' b),PA,G)) . z) '&' ((All ((a 'imp' ('not' b)),PA,G)) . z)) by MARGREL1:def_20 ;
assume A2: (Ex (a,PA,G)) . z = TRUE ; ::_thesis: ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_a_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A2, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: a . x1 = TRUE ;
A5: (a 'imp' b) . x1 = ('not' TRUE) 'or' (b . x1) by A4, BVFUNC_1:def_8
.= FALSE 'or' (b . x1) by MARGREL1:11
.= b . x1 by BINARITH:3 ;
A6: (a 'imp' ('not' b)) . x1 = ('not' TRUE) 'or' (('not' b) . x1) by A4, BVFUNC_1:def_8
.= FALSE 'or' (('not' b) . x1) by MARGREL1:11
.= ('not' b) . x1 by BINARITH:3 ;
percases ( b . x1 = TRUE or b . x1 = FALSE ) by XBOOLEAN:def_3;
suppose b . x1 = TRUE ; ::_thesis: ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = TRUE
then (a 'imp' ('not' b)) . x1 = 'not' TRUE by A6, MARGREL1:def_19
.= FALSE by MARGREL1:11 ;
then  (B_INF ((a 'imp' ('not' b)),(CompF (PA,G)))) . z = FALSE by A3, BVFUNC_1:def_16;
hence ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = 'not' (((All ((a 'imp' b),PA,G)) . z) '&' FALSE) by A1, BVFUNC_2:def_9
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ;
::_thesis: verum
end;
suppose b . x1 = FALSE ; ::_thesis: ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = TRUE
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by A3, A5, BVFUNC_1:def_16;
hence ('not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))) . z = 'not' (FALSE '&' ((All ((a 'imp' ('not' b)),PA,G)) . z)) by A1, BVFUNC_2:def_9
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:29
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) '<' 'not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' 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) '<' 'not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' 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) '<' 'not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex (a,PA,G) '<' 'not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))
let PA be a_partition of Y; ::_thesis: Ex (a,PA,G) '<' 'not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex (a,PA,G)) . z = TRUE or ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = TRUE )
A1: ('not' (Ex ((a '&' ('not' b)),PA,G))) . z = 'not' ((Ex ((a '&' ('not' b)),PA,G)) . z) by MARGREL1:def_19;
A2: ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = 'not' ((('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G)))) . z) by MARGREL1:def_19
.= 'not' ((('not' (Ex ((a '&' b),PA,G))) . z) '&' (('not' (Ex ((a '&' ('not' b)),PA,G))) . z)) by MARGREL1:def_20
.= 'not' (('not' ((Ex ((a '&' b),PA,G)) . z)) '&' ('not' ((Ex ((a '&' ('not' b)),PA,G)) . z))) by A1, MARGREL1:def_19 ;
assume A3: (Ex (a,PA,G)) . z = TRUE ; ::_thesis: ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = TRUE
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_a_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  contradiction by A3, BVFUNC_2:def_10; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (PA,G))) and
A5: a . x1 = TRUE ;
A6: (a '&' b) . x1 = TRUE '&' (b . x1) by A5, MARGREL1:def_20
.= b . x1 by MARGREL1:14 ;
A7: (a '&' ('not' b)) . x1 = TRUE '&' (('not' b) . x1) by A5, MARGREL1:def_20
.= ('not' b) . x1 by MARGREL1:14 ;
percases ( b . x1 = TRUE or b . x1 = FALSE ) by XBOOLEAN:def_3;
suppose b . x1 = TRUE ; ::_thesis: ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = TRUE
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A4, A6, BVFUNC_1:def_17;
hence ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = 'not' (('not' TRUE) '&' ('not' ((Ex ((a '&' ('not' b)),PA,G)) . z))) by A2, BVFUNC_2:def_10
.= 'not' (FALSE '&' ('not' ((Ex ((a '&' ('not' b)),PA,G)) . z))) by MARGREL1:11
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ;
::_thesis: verum
end;
suppose b . x1 = FALSE ; ::_thesis: ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = TRUE
then  (a '&' ('not' b)) . x1 = 'not' FALSE by A7, MARGREL1:def_19;
then  (a '&' ('not' b)) . x1 = TRUE by MARGREL1:11;
then  (B_SUP ((a '&' ('not' b)),(CompF (PA,G)))) . z = TRUE by A4, BVFUNC_1:def_17;
hence ('not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))) . z = 'not' (('not' ((Ex ((a '&' b),PA,G)) . z)) '&' ('not' TRUE)) by A2, BVFUNC_2:def_10
.= 'not' (('not' ((Ex ((a '&' b),PA,G)) . z)) '&' FALSE) by MARGREL1:11
.= 'not' FALSE by MARGREL1:12
.= TRUE by MARGREL1:11 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:30
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)) '&' (All ((a 'imp' b),PA,G)) '<' Ex ((a '&' 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)) '&' (All ((a 'imp' b),PA,G)) '<' Ex ((a '&' 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)) '&' (All ((a 'imp' b),PA,G)) '<' Ex ((a '&' b),PA,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) '&' (All ((a 'imp' b),PA,G)) '<' Ex ((a '&' b),PA,G)
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) '&' (All ((a 'imp' b),PA,G)) '<' Ex ((a '&' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) '&' (All ((a 'imp' b),PA,G))) . z = TRUE or (Ex ((a '&' b),PA,G)) . z = TRUE )
A1: 'not' FALSE = TRUE by MARGREL1:11;
assume  ((Ex (a,PA,G)) '&' (All ((a 'imp' b),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then A2: ((Ex (a,PA,G)) . z) '&' ((All ((a 'imp' b),PA,G)) . z) = TRUE by MARGREL1:def_20;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_a_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: a . x1 = TRUE ;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((a 'imp' b),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then  (a 'imp' b) . x1 = TRUE by A3;
then A5: ('not' (a . x1)) 'or' (b . x1) = TRUE by BVFUNC_1:def_8;
(a '&' b) . x1 = (a . x1) '&' (b . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A4, A5, A1, BINARITH:3
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A3, BVFUNC_1:def_17;
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;

theorem :: BVFUNC_3:31
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)) '&' ('not' (Ex ((a '&' b),PA,G))) '<' 'not' (All ((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)) '&' ('not' (Ex ((a '&' b),PA,G))) '<' 'not' (All ((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)) '&' ('not' (Ex ((a '&' b),PA,G))) '<' 'not' (All ((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)) '&' ('not' (Ex ((a '&' b),PA,G))) '<' 'not' (All ((a 'imp' b),PA,G))
let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) '&' ('not' (Ex ((a '&' b),PA,G))) '<' 'not' (All ((a 'imp' b),PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) '&' ('not' (Ex ((a '&' b),PA,G)))) . z = TRUE or ('not' (All ((a 'imp' b),PA,G))) . z = TRUE )
assume  ((Ex (a,PA,G)) '&' ('not' (Ex ((a '&' b),PA,G)))) . z = TRUE ; ::_thesis: ('not' (All ((a 'imp' b),PA,G))) . z = TRUE
then A1: ((Ex (a,PA,G)) . z) '&' (('not' (Ex ((a '&' b),PA,G))) . z) = TRUE by MARGREL1:def_20;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_a_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (a,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A2: x1 in EqClass (z,(CompF (PA,G))) and
A3: a . x1 = TRUE ;
 ('not' (Ex ((a '&' b),PA,G))) . z = TRUE by A1, MARGREL1:12;
then  'not' ((Ex ((a '&' b),PA,G)) . z) = TRUE by MARGREL1:def_19;
then  ( Ex ((a '&' b),PA,G) = B_SUP ((a '&' b),(CompF (PA,G))) & (Ex ((a '&' b),PA,G)) . z = FALSE ) by BVFUNC_2:def_10, MARGREL1:11;
then  (a '&' b) . x1 <> TRUE by A2, BVFUNC_1:def_17;
then  (a '&' b) . x1 = FALSE by XBOOLEAN:def_3;
then A4: (a . x1) '&' (b . x1) = FALSE by MARGREL1:def_20;
percases ( a . x1 = FALSE or b . x1 = FALSE ) by A4, MARGREL1:12;
suppose a . x1 = FALSE ; ::_thesis: ('not' (All ((a 'imp' b),PA,G))) . z = TRUE
hence  ('not' (All ((a 'imp' b),PA,G))) . z = TRUE by A3; ::_thesis: verum
end;
suppose b . x1 = FALSE ; ::_thesis: ('not' (All ((a 'imp' b),PA,G))) . z = TRUE
then (a 'imp' b) . x1 = ('not' TRUE) 'or' FALSE by A3, BVFUNC_1:def_8
.= FALSE 'or' FALSE by MARGREL1:11
.= FALSE ;
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by A2, BVFUNC_1:def_16;
then  (All ((a 'imp' b),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence ('not' (All ((a 'imp' b),PA,G))) . z = 'not' FALSE by MARGREL1:def_19
.= TRUE by MARGREL1:11 ;
::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:32
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, c, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G)) '<' All ((a 'imp' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for a, c, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G)) '<' All ((a 'imp' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for a, c, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G)) '<' All ((a 'imp' b),PA,G)
let a, c, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G)) '<' All ((a 'imp' b),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G)) '<' All ((a 'imp' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G))) . z = TRUE or (All ((a 'imp' b),PA,G)) . z = TRUE )
assume  ((All ((a 'imp' c),PA,G)) '&' (All ((c 'imp' b),PA,G))) . z = TRUE ; ::_thesis: (All ((a 'imp' b),PA,G)) . z = TRUE
then A1: ((All ((a 'imp' c),PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z) = TRUE by MARGREL1:def_20;
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' b),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_c)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'imp' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((a 'imp' c),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' b) . x = TRUE )
A4: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3;
A5: ( 'not' (c . x) = TRUE or 'not' (c . x) = FALSE ) by XBOOLEAN:def_3;
assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' b) . x = TRUE
then  (a 'imp' c) . x = TRUE by A3;
then A7: ('not' (a . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8;
 (c 'imp' b) . x = TRUE by A2, A6;
then A8: ('not' (c . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
percases ( ( 'not' (a . x) = TRUE & 'not' (c . x) = TRUE ) or ( 'not' (a . x) = TRUE & b . x = TRUE ) or ( c . x = TRUE & 'not' (c . x) = TRUE ) or ( c . x = TRUE & b . x = TRUE ) ) by A7, A4, A8, A5, BINARITH:3;
suppose ( 'not' (a . x) = TRUE & 'not' (c . x) = TRUE ) ; ::_thesis: (a 'imp' b) . x = TRUE
hence (a 'imp' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( 'not' (a . x) = TRUE & b . x = TRUE ) ; ::_thesis: (a 'imp' b) . x = TRUE
hence (a 'imp' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( c . x = TRUE & 'not' (c . x) = TRUE ) ; ::_thesis: (a 'imp' b) . x = TRUE
hence  (a 'imp' b) . x = TRUE by MARGREL1:11; ::_thesis: verum
end;
suppose ( c . x = TRUE & b . x = TRUE ) ; ::_thesis: (a 'imp' b) . x = TRUE
hence (a 'imp' b) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' b),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:33
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' b),PA,G)
let c, b, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' b),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G))) . z = TRUE or (Ex ((a '&' b),PA,G)) . z = TRUE )
assume  ((All ((c 'imp' b),PA,G)) '&' (Ex ((a '&' c),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then A1: ((All ((c 'imp' b),PA,G)) . z) '&' ((Ex ((a '&' c),PA,G)) . z) = TRUE by MARGREL1:def_20;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'&'_c)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (a '&' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((a '&' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex ((a '&' c),PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A2: x1 in EqClass (z,(CompF (PA,G))) and
A3: (a '&' c) . x1 = TRUE ;
A4: (a . x1) '&' (c . x1) = TRUE by A3, MARGREL1:def_20;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' b),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then  (c 'imp' b) . x1 = TRUE by A2;
then A5: ('not' (c . x1)) 'or' (b . x1) = TRUE by BVFUNC_1:def_8;
A6: ( 'not' (c . x1) = TRUE or 'not' (c . x1) = FALSE ) by XBOOLEAN:def_3;
percases ( ( a . x1 = TRUE & c . x1 = TRUE & 'not' (c . x1) = TRUE ) or ( a . x1 = TRUE & c . x1 = TRUE & b . x1 = TRUE ) ) by A5, A6, A4, BINARITH:3, MARGREL1:12;
suppose ( a . x1 = TRUE & c . x1 = TRUE & 'not' (c . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by MARGREL1:11; ::_thesis: verum
end;
suppose ( a . x1 = TRUE & c . x1 = TRUE & b . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then (a '&' b) . x1 = TRUE '&' TRUE by MARGREL1:def_20
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:34
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let b, c, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G))) . z = TRUE or (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE )
assume  ((All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G))) . z = TRUE ; ::_thesis: (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE
then A1: ((All ((b 'imp' ('not' c)),PA,G)) . z) '&' ((All ((a 'imp' c),PA,G)) . z) = TRUE by MARGREL1:def_20;
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_c)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'imp' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((a 'imp' c),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_('not'_c))_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' ('not' c)) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' ('not' c)),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' ('not' c)),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' ('not' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' ('not' b)) . x = TRUE )
A4: ( 'not' (b . x) = TRUE or 'not' (b . x) = FALSE ) by XBOOLEAN:def_3;
A5: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3;
assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  (b 'imp' ('not' c)) . x = TRUE by A3;
then A7: ('not' (b . x)) 'or' (('not' c) . x) = TRUE by BVFUNC_1:def_8;
 (a 'imp' c) . x = TRUE by A2, A6;
then A8: ('not' (a . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8;
percases ( ( 'not' (b . x) = TRUE & 'not' (a . x) = TRUE ) or ( 'not' (b . x) = TRUE & c . x = TRUE ) or ( ('not' c) . x = TRUE & 'not' (a . x) = TRUE ) or ( ('not' c) . x = TRUE & c . x = TRUE ) ) by A7, A4, A8, A5, BINARITH:3;
supposeA9: ( 'not' (b . x) = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  ('not' b) . x = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = TRUE 'or' TRUE by A9, BVFUNC_1:def_8
.= TRUE ;
::_thesis: verum
end;
suppose ( 'not' (b . x) = TRUE & c . x = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  ('not' b) . x = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( ('not' c) . x = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
hence (a 'imp' ('not' b)) . x = TRUE 'or' (('not' b) . x) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA10: ( ('not' c) . x = TRUE & c . x = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  'not' (c . x) = TRUE by MARGREL1:def_19;
hence  (a 'imp' ('not' b)) . x = TRUE by A10, MARGREL1:11; ::_thesis: verum
end;
end;
end;
then  (B_INF ((a 'imp' ('not' b)),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:35
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let b, c, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G))) . z = TRUE or (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE )
assume  ((All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G))) . z = TRUE ; ::_thesis: (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE
then A1: ((All ((b 'imp' c),PA,G)) . z) '&' ((All ((a 'imp' ('not' c)),PA,G)) . z) = TRUE by MARGREL1:def_20;
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_('not'_c))_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (a 'imp' ('not' c)) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' ('not' c)),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((a 'imp' ('not' c)),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_c)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' c),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' ('not' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' ('not' b)) . x = TRUE )
A4: ( 'not' (b . x) = TRUE or 'not' (b . x) = FALSE ) by XBOOLEAN:def_3;
A5: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3;
assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  (b 'imp' c) . x = TRUE by A3;
then A7: ('not' (b . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8;
 (a 'imp' ('not' c)) . x = TRUE by A2, A6;
then A8: ('not' (a . x)) 'or' (('not' c) . x) = TRUE by BVFUNC_1:def_8;
percases ( ( 'not' (b . x) = TRUE & 'not' (a . x) = TRUE ) or ( 'not' (b . x) = TRUE & ('not' c) . x = TRUE ) or ( c . x = TRUE & 'not' (a . x) = TRUE ) or ( c . x = TRUE & ('not' c) . x = TRUE ) ) by A7, A4, A8, A5, BINARITH:3;
supposeA9: ( 'not' (b . x) = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  ('not' b) . x = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = TRUE 'or' TRUE by A9, BVFUNC_1:def_8
.= TRUE ;
::_thesis: verum
end;
suppose ( 'not' (b . x) = TRUE & ('not' c) . x = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  ('not' b) . x = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( c . x = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
hence (a 'imp' ('not' b)) . x = TRUE 'or' (('not' b) . x) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
supposeA10: ( c . x = TRUE & ('not' c) . x = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  'not' (c . x) = TRUE by MARGREL1:def_19;
hence  (a 'imp' ('not' b)) . x = TRUE by A10, MARGREL1:11; ::_thesis: verum
end;
end;
end;
then  (B_INF ((a 'imp' ('not' b)),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:36
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let b, c, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G))) . z = TRUE or (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE )
assume  ((All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
then A1: ((All ((b 'imp' ('not' c)),PA,G)) . z) '&' ((Ex ((a '&' c),PA,G)) . z) = TRUE by MARGREL1:def_20;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'&'_c)_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (a '&' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((a '&' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex ((a '&' c),PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A2: x1 in EqClass (z,(CompF (PA,G))) and
A3: (a '&' c) . x1 = TRUE ;
A4: (a . x1) '&' (c . x1) = TRUE by A3, MARGREL1:def_20;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_('not'_c))_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' ('not' c)) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' ('not' c)),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' ('not' c)),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then  (b 'imp' ('not' c)) . x1 = TRUE by A2;
then A5: ('not' (b . x1)) 'or' (('not' c) . x1) = TRUE by BVFUNC_1:def_8;
A6: ( 'not' (b . x1) = TRUE or 'not' (b . x1) = FALSE ) by XBOOLEAN:def_3;
percases ( ( a . x1 = TRUE & c . x1 = TRUE & 'not' (b . x1) = TRUE ) or ( a . x1 = TRUE & c . x1 = TRUE & ('not' c) . x1 = TRUE ) ) by A5, A6, A4, BINARITH:3, MARGREL1:12;
supposeA7: ( a . x1 = TRUE & c . x1 = TRUE & 'not' (b . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
(a '&' ('not' b)) . x1 = (a . x1) '&' (('not' b) . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A7, MARGREL1:def_19
.= TRUE ;
then  (B_SUP ((a '&' ('not' b)),(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
supposeA8: ( a . x1 = TRUE & c . x1 = TRUE & ('not' c) . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
then  'not' (c . x1) = TRUE by MARGREL1:def_19;
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by A8, MARGREL1:11; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:37
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let b, c, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G))) . z = TRUE or (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE )
assume  ((All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
then A1: ((All ((b 'imp' c),PA,G)) . z) '&' ((Ex ((a '&' ('not' c)),PA,G)) . z) = TRUE by MARGREL1:def_20;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'&'_('not'_c))_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not (a '&' ('not' c)) . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP ((a '&' ('not' c)),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex ((a '&' ('not' c)),PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A2: x1 in EqClass (z,(CompF (PA,G))) and
A3: (a '&' ('not' c)) . x1 = TRUE ;
A4: (a . x1) '&' (('not' c) . x1) = TRUE by A3, MARGREL1:def_20;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_c)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' c),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then  (b 'imp' c) . x1 = TRUE by A2;
then A5: ('not' (b . x1)) 'or' (c . x1) = TRUE by BVFUNC_1:def_8;
A6: ( 'not' (b . x1) = TRUE or 'not' (b . x1) = FALSE ) by XBOOLEAN:def_3;
percases ( ( a . x1 = TRUE & ('not' c) . x1 = TRUE & 'not' (b . x1) = TRUE ) or ( a . x1 = TRUE & ('not' c) . x1 = TRUE & c . x1 = TRUE ) ) by A5, A6, A4, BINARITH:3, MARGREL1:12;
supposeA7: ( a . x1 = TRUE & ('not' c) . x1 = TRUE & 'not' (b . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
(a '&' ('not' b)) . x1 = (a . x1) '&' (('not' b) . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A7, MARGREL1:def_19
.= TRUE ;
then  (B_SUP ((a '&' ('not' b)),(CompF (PA,G)))) . z = TRUE by A2, BVFUNC_1:def_17;
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
supposeA8: ( a . x1 = TRUE & ('not' c) . x1 = TRUE & c . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
then  'not' (c . x1) = TRUE by MARGREL1:def_19;
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by A8, MARGREL1:11; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:38
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let c, b, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let PA be a_partition of Y; ::_thesis: ((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z = TRUE or (Ex ((a '&' b),PA,G)) . z = TRUE )
assume  (((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then A1: (((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) . z) '&' ((All ((c 'imp' a),PA,G)) . z) = TRUE by MARGREL1:def_20;
then  (((Ex (c,PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z)) '&' ((All ((c 'imp' a),PA,G)) . z) = TRUE by MARGREL1:def_20;
then A2: ((Ex (c,PA,G)) . z) '&' ((All ((c 'imp' b),PA,G)) . z) = TRUE by MARGREL1:12;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_c_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not c . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (c,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (c,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: c . x1 = TRUE ;
A5: ( 'not' (c . x1) = TRUE or 'not' (c . x1) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_b)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' b),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then  (c 'imp' b) . x1 = TRUE by A3;
then A6: ('not' (c . x1)) 'or' (b . x1) = TRUE by BVFUNC_1:def_8;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_a)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' a) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' a),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' a),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then  (c 'imp' a) . x1 = TRUE by A3;
then A7: ('not' (c . x1)) 'or' (a . x1) = TRUE by BVFUNC_1:def_8;
percases ( 'not' (c . x1) = TRUE or ( 'not' (c . x1) = TRUE & b . x1 = TRUE ) or ( a . x1 = TRUE & 'not' (c . x1) = TRUE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by A7, A5, A6, BINARITH:3;
suppose 'not' (c . x1) = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
suppose ( 'not' (c . x1) = TRUE & b . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
suppose ( a . x1 = TRUE & 'not' (c . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
suppose ( a . x1 = TRUE & b . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then (a '&' b) . x1 = TRUE '&' TRUE by MARGREL1:def_20
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A3, BVFUNC_1:def_17;
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:39
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let b, c, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let PA be a_partition of Y; ::_thesis: (All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G))) . z = TRUE or (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE )
assume  ((All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G))) . z = TRUE ; ::_thesis: (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE
then A1: ((All ((b 'imp' c),PA,G)) . z) '&' ((All ((c 'imp' ('not' a)),PA,G)) . z) = TRUE by MARGREL1:def_20;
A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_c)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' c),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_('not'_a))_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' ('not' a)) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' ('not' a)),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' ('not' a)),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
 for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' ('not' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' ('not' b)) . x = TRUE )
A4: ( 'not' (c . x) = TRUE or 'not' (c . x) = FALSE ) by XBOOLEAN:def_3;
A5: ( 'not' (b . x) = TRUE or 'not' (b . x) = FALSE ) by XBOOLEAN:def_3;
assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  (c 'imp' ('not' a)) . x = TRUE by A3;
then A7: ('not' (c . x)) 'or' (('not' a) . x) = TRUE by BVFUNC_1:def_8;
 (b 'imp' c) . x = TRUE by A2, A6;
then A8: ('not' (b . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8;
percases ( ( 'not' (c . x) = TRUE & 'not' (b . x) = TRUE ) or ( 'not' (c . x) = TRUE & c . x = TRUE ) or ( ('not' a) . x = TRUE & 'not' (b . x) = TRUE ) or ( ('not' a) . x = TRUE & c . x = TRUE ) ) by A7, A4, A8, A5, BINARITH:3;
suppose ( 'not' (c . x) = TRUE & 'not' (b . x) = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  ('not' b) . x = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( 'not' (c . x) = TRUE & c . x = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
hence  (a 'imp' ('not' b)) . x = TRUE by MARGREL1:11; ::_thesis: verum
end;
suppose ( ('not' a) . x = TRUE & 'not' (b . x) = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  ('not' b) . x = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
suppose ( ('not' a) . x = TRUE & c . x = TRUE ) ; ::_thesis: (a 'imp' ('not' b)) . x = TRUE
then  'not' (a . x) = TRUE by MARGREL1:def_19;
hence (a 'imp' ('not' b)) . x = TRUE 'or' (('not' b) . x) by BVFUNC_1:def_8
.= TRUE by BINARITH:10 ;
::_thesis: verum
end;
end;
end;
then  (B_INF ((a 'imp' ('not' b)),(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  (All ((a 'imp' ('not' b)),PA,G)) . z = TRUE by BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:40
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let b, c, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds ((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let PA be a_partition of Y; ::_thesis: ((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' b),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z = TRUE or (Ex ((a '&' b),PA,G)) . z = TRUE )
assume  (((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then A1: (((Ex (b,PA,G)) '&' (All ((b 'imp' c),PA,G))) . z) '&' ((All ((c 'imp' a),PA,G)) . z) = TRUE by MARGREL1:def_20;
then  (((Ex (b,PA,G)) . z) '&' ((All ((b 'imp' c),PA,G)) . z)) '&' ((All ((c 'imp' a),PA,G)) . z) = TRUE by MARGREL1:def_20;
then A2: ((Ex (b,PA,G)) . z) '&' ((All ((b 'imp' c),PA,G)) . z) = TRUE by MARGREL1:12;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_b_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (b,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: b . x1 = TRUE ;
A5: ( 'not' (c . x1) = TRUE or 'not' (c . x1) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_a)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' a) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' a),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' a),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then  (c 'imp' a) . x1 = TRUE by A3;
then A6: ('not' (c . x1)) 'or' (a . x1) = TRUE by BVFUNC_1:def_8;
A7: ( 'not' (b . x1) = TRUE or 'not' (b . x1) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_c)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' c) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' c),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' c),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then  (b 'imp' c) . x1 = TRUE by A3;
then A8: ('not' (b . x1)) 'or' (c . x1) = TRUE by BVFUNC_1:def_8;
percases ( ( 'not' (c . x1) = TRUE & 'not' (b . x1) = TRUE ) or ( 'not' (c . x1) = TRUE & c . x1 = TRUE ) or ( a . x1 = TRUE & 'not' (b . x1) = TRUE ) or ( a . x1 = TRUE & c . x1 = TRUE ) ) by A6, A5, A8, A7, BINARITH:3;
suppose ( 'not' (c . x1) = TRUE & 'not' (b . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
suppose ( 'not' (c . x1) = TRUE & c . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by MARGREL1:11; ::_thesis: verum
end;
suppose ( a . x1 = TRUE & 'not' (b . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
suppose ( a . x1 = TRUE & c . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' b),PA,G)) . z = TRUE
then (a '&' b) . x1 = TRUE '&' TRUE by A4, MARGREL1:def_20
.= TRUE ;
then  (B_SUP ((a '&' b),(CompF (PA,G)))) . z = TRUE by A3, BVFUNC_1:def_17;
hence  (Ex ((a '&' b),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_3:41
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let c, b, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let PA be a_partition of Y; ::_thesis: ((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z = TRUE or (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE )
assume  (((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G))) . z = TRUE ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
then A1: (((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) . z) '&' ((All ((c 'imp' a),PA,G)) . z) = TRUE by MARGREL1:def_20;
then  (((Ex (c,PA,G)) . z) '&' ((All ((b 'imp' ('not' c)),PA,G)) . z)) '&' ((All ((c 'imp' a),PA,G)) . z) = TRUE by MARGREL1:def_20;
then A2: ((Ex (c,PA,G)) . z) '&' ((All ((b 'imp' ('not' c)),PA,G)) . z) = TRUE by MARGREL1:12;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_c_._x_=_TRUE_)
assume  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not c . x = TRUE ) ; ::_thesis: contradiction
then  (B_SUP (c,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
then  (Ex (c,PA,G)) . z = FALSE by BVFUNC_2:def_10;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: c . x1 = TRUE ;
A5: ( 'not' (c . x1) = TRUE or 'not' (c . x1) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(c_'imp'_a)_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (c 'imp' a) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((c 'imp' a),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((c 'imp' a),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A1, MARGREL1:12; ::_thesis: verum
end;
then  (c 'imp' a) . x1 = TRUE by A3;
then A6: ('not' (c . x1)) 'or' (a . x1) = TRUE by BVFUNC_1:def_8;
A7: ( 'not' (b . x1) = TRUE or 'not' (b . x1) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(b_'imp'_('not'_c))_._x_=_TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not (b 'imp' ('not' c)) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((b 'imp' ('not' c)),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
then  (All ((b 'imp' ('not' c)),PA,G)) . z = FALSE by BVFUNC_2:def_9;
hence  contradiction by A2, MARGREL1:12; ::_thesis: verum
end;
then  (b 'imp' ('not' c)) . x1 = TRUE by A3;
then A8: ('not' (b . x1)) 'or' (('not' c) . x1) = TRUE by BVFUNC_1:def_8;
percases ( ( 'not' (c . x1) = TRUE & 'not' (b . x1) = TRUE ) or ( 'not' (c . x1) = TRUE & ('not' c) . x1 = TRUE ) or ( a . x1 = TRUE & 'not' (b . x1) = TRUE ) or ( a . x1 = TRUE & ('not' c) . x1 = TRUE ) ) by A6, A5, A8, A7, BINARITH:3;
suppose ( 'not' (c . x1) = TRUE & 'not' (b . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
suppose ( 'not' (c . x1) = TRUE & ('not' c) . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
supposeA9: ( a . x1 = TRUE & 'not' (b . x1) = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
(a '&' ('not' b)) . x1 = (a . x1) '&' (('not' b) . x1) by MARGREL1:def_20
.= TRUE '&' TRUE by A9, MARGREL1:def_19
.= TRUE ;
then  (B_SUP ((a '&' ('not' b)),(CompF (PA,G)))) . z = TRUE by A3, BVFUNC_1:def_17;
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
end;
suppose ( a . x1 = TRUE & ('not' c) . x1 = TRUE ) ; ::_thesis: (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE
then  'not' (c . x1) = TRUE by MARGREL1:def_19;
hence  (Ex ((a '&' ('not' b)),PA,G)) . z = TRUE by A4, MARGREL1:11; ::_thesis: verum
end;
end;
end;