:: BVFUNC_4 semantic presentation

begin

theorem :: BVFUNC_4:1
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '<' b 'imp' c holds
a '&' b '<' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a '<' b 'imp' c holds
a '&' b '<' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '<' b 'imp' c implies a '&' b '<' c )
assume A1: a '<' b 'imp' c ; ::_thesis: a '&' b '<' c
 for x being Element of Y holds ((a '&' b) 'imp' c) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' b) 'imp' c) . x = TRUE
A2: (a 'imp' (b 'imp' c)) . x = ('not' (a . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) ;
A3: ((a '&' b) 'imp' c) . x = ('not' ((a '&' b) . x)) 'or' (c . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) by MARGREL1:def_20 ;
 a 'imp' (b 'imp' c) = I_el Y by A1, BVFUNC_1:16;
hence  ((a '&' b) 'imp' c) . x = TRUE by A2, A3, BVFUNC_1:def_11; ::_thesis: verum
end;
then  (a '&' b) 'imp' c = I_el Y by BVFUNC_1:def_11;
hence  a '&' b '<' c by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_4:2
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '<' b 'imp' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '<' b 'imp' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '&' b '<' c implies a '<' b 'imp' c )
assume A1: a '&' b '<' c ; ::_thesis: a '<' b 'imp' c
 for x being Element of Y holds (a 'imp' (b 'imp' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' (b 'imp' c)) . x = TRUE
A2: (a 'imp' (b 'imp' c)) . x = ('not' (a . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) ;
A3: ((a '&' b) 'imp' c) . x = ('not' ((a '&' b) . x)) 'or' (c . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) by MARGREL1:def_20 ;
 (a '&' b) 'imp' c = I_el Y by A1, BVFUNC_1:16;
hence  (a 'imp' (b 'imp' c)) . x = TRUE by A2, A3, BVFUNC_1:def_11; ::_thesis: verum
end;
then  a 'imp' (b 'imp' c) = I_el Y by BVFUNC_1:def_11;
hence  a '<' b 'imp' c by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_4:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' (a '&' b) = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' (a '&' b)) . x = a . x
thus (a 'or' (a '&' b)) . x = (a . x) 'or' ((a '&' b) . x) by BVFUNC_1:def_4
.= (a . x) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_20
.= a . x by XBOOLEAN:5 ; ::_thesis: verum
end;

theorem :: BVFUNC_4:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' (a 'or' b) = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' (a 'or' b)) . x = a . x
thus (a '&' (a 'or' b)) . x = (a . x) '&' ((a 'or' b) . x) by MARGREL1:def_20
.= (a . x) '&' ((a . x) 'or' (b . x)) by BVFUNC_1:def_4
.= a . x by XBOOLEAN:6 ; ::_thesis: verum
end;

theorem Th5: :: BVFUNC_4:5
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' ('not' a) = O_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a '&' ('not' a) = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a '&' ('not' a) = O_el Y
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' ('not' a)) . x = (O_el Y) . x
thus (a '&' ('not' a)) . x = (a . x) '&' (('not' a) . x) by MARGREL1:def_20
.= (a . x) '&' ('not' (a . x)) by MARGREL1:def_19
.= FALSE by XBOOLEAN:138
.= (O_el Y) . x by BVFUNC_1:def_10 ; ::_thesis: verum
end;

theorem :: BVFUNC_4:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' ('not' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'or' ('not' a) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'or' ('not' a) = I_el Y
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' ('not' a)) . x = (I_el Y) . x
thus (a 'or' ('not' a)) . x = (a . x) 'or' (('not' a) . x) by BVFUNC_1:def_4
.= (a . x) 'or' ('not' (a . x)) by MARGREL1:def_19
.= TRUE by XBOOLEAN:102
.= (I_el Y) . x by BVFUNC_1:def_11 ; ::_thesis: verum
end;

theorem Th7: :: BVFUNC_4:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = (a 'imp' b) '&' (b 'imp' a)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' b) . x = ((a 'imp' b) '&' (b 'imp' a)) . x
thus (a 'eqv' b) . x = (a . x) <=> (b . x) by BVFUNC_1:def_9
.= ((a . x) => (b . x)) '&' ((b . x) => (a . x))
.= ((a 'imp' b) . x) '&' ((b . x) => (a . x)) by BVFUNC_1:def_8
.= ((a 'imp' b) . x) '&' ((b 'imp' a) . x) by BVFUNC_1:def_8
.= ((a 'imp' b) '&' (b 'imp' a)) . x by MARGREL1:def_20 ; ::_thesis: verum
end;

theorem Th8: :: BVFUNC_4:8
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' a) 'or' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' a) 'or' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = ('not' a) 'or' b
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' b) . x = (('not' a) 'or' b) . x
thus (a 'imp' b) . x = (a . x) => (b . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' (b . x)
.= (('not' a) . x) 'or' (b . x) by MARGREL1:def_19
.= (('not' a) 'or' b) . x by BVFUNC_1:def_4 ; ::_thesis: verum
end;

theorem :: BVFUNC_4:9
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' b) . x = ((('not' a) '&' b) 'or' (a '&' ('not' b))) . x
thus (a 'xor' b) . x = (a . x) 'xor' (b . x) by BVFUNC_1:def_5
.= (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x)))
.= (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_19
.= ((('not' a) . x) '&' (b . x)) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_19
.= ((('not' a) '&' b) . x) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_20
.= ((('not' a) '&' b) . x) 'or' ((a '&' ('not' b)) . x) by MARGREL1:def_20
.= ((('not' a) '&' b) 'or' (a '&' ('not' b))) . x by BVFUNC_1:def_4 ; ::_thesis: verum
end;

theorem Th10: :: BVFUNC_4:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) )
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) )
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) )
thus  ( a 'eqv' b = I_el Y implies ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) ::_thesis: ( a 'imp' b = I_el Y & b 'imp' a = I_el Y implies a 'eqv' b = I_el Y )
proof
assume  a 'eqv' b = I_el Y ; ::_thesis: ( a 'imp' b = I_el Y & b 'imp' a = I_el Y )
then  a = b by BVFUNC_1:17;
hence  ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) by BVFUNC_1:16; ::_thesis: verum
end;
assume  ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ; ::_thesis: a 'eqv' b = I_el Y
then  a 'eqv' b = (I_el Y) '&' (I_el Y) by Th7;
hence  a 'eqv' b = I_el Y ; ::_thesis: verum
end;

theorem :: BVFUNC_4:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
('not' a) 'eqv' ('not' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
('not' a) 'eqv' ('not' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y implies ('not' a) 'eqv' ('not' b) = I_el Y )
assume  a 'eqv' b = I_el Y ; ::_thesis: ('not' a) 'eqv' ('not' b) = I_el Y
then  a = b by BVFUNC_1:17;
hence  ('not' a) 'eqv' ('not' b) = I_el Y by BVFUNC_1:17; ::_thesis: verum
end;

theorem :: BVFUNC_4:12
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a '&' c) 'eqv' (b '&' d) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a '&' c) 'eqv' (b '&' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a '&' c) 'eqv' (b '&' d) = I_el Y )
assume  ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a '&' c) 'eqv' (b '&' d) = I_el Y
then  ( a = b & c = d ) by BVFUNC_1:17;
hence  (a '&' c) 'eqv' (b '&' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum
end;

theorem :: BVFUNC_4:13
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'imp' c) 'eqv' (b 'imp' d) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'imp' c) 'eqv' (b 'imp' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y )
assume  ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y
then  ( a = b & c = d ) by BVFUNC_1:17;
hence  (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum
end;

theorem :: BVFUNC_4:14
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'or' c) 'eqv' (b 'or' d) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'or' c) 'eqv' (b 'or' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a 'or' c) 'eqv' (b 'or' d) = I_el Y )
assume  ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a 'or' c) 'eqv' (b 'or' d) = I_el Y
then  ( a = b & c = d ) by BVFUNC_1:17;
hence  (a 'or' c) 'eqv' (b 'or' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum
end;

theorem :: BVFUNC_4:15
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y )
assume  ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y
then  ( a = b & c = d ) by BVFUNC_1:17;
hence  (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum
end;

begin

theorem :: BVFUNC_4:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (All ((a 'eqv' b),PA,G)) . z = ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z
(All ((a 'eqv' b),PA,G)) . z = (All (((a 'imp' b) '&' (b 'imp' a)),PA,G)) . z by Th7
.= ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z by BVFUNC_1:39 ;
hence  (All ((a 'eqv' b),PA,G)) . z = ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z ; ::_thesis: verum
end;

theorem :: BVFUNC_4:17
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)
let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)
let PA, PB be a_partition of Y; ::_thesis: All (a,PA,G) '<' Ex (a,PB,G)
 ( All (a,PA,G) '<' a & a '<' Ex (a,PB,G) ) by BVFUNC_2:11, BVFUNC_2:12;
hence  All (a,PA,G) '<' Ex (a,PB,G) by BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_4:18
for Y being non empty set
for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
let a, u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
let PA be a_partition of Y; ::_thesis: ( a 'imp' u = I_el Y implies (All (a,PA,G)) 'imp' u = I_el Y )
assume A1: a 'imp' u = I_el Y ; ::_thesis: (All (a,PA,G)) 'imp' u = I_el Y
 for x being Element of Y holds ((All (a,PA,G)) 'imp' u) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE
 (a 'imp' u) . x = TRUE by A1, BVFUNC_1:def_11;
then A2: ('not' (a . x)) 'or' (u . x) = TRUE by BVFUNC_1:def_8;
A3: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_((All_(a,PA,G))_'imp'_u)_._x_=_TRUE_)_or_(_u_._x_=_TRUE_&_((All_(a,PA,G))_'imp'_u)_._x_=_TRUE_)_)
percases ( 'not' (a . x) = TRUE or u . x = TRUE ) by A2, A3;
caseA4: 'not' (a . x) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE
 x in EqClass (x,(CompF (PA,G))) by EQREL_1:def_6;
then  (B_INF (a,(CompF (PA,G)))) . x = FALSE by A4, BVFUNC_1:def_16;
then ((All (a,PA,G)) 'imp' u) . x = TRUE 'or' (u . x) by BVFUNC_1:def_8
.= TRUE ;
hence  ((All (a,PA,G)) 'imp' u) . x = TRUE ; ::_thesis: verum
end;
case u . x = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE
then ((All (a,PA,G)) 'imp' u) . x = ('not' ((All (a,PA,G)) . x)) 'or' TRUE by BVFUNC_1:def_8
.= TRUE ;
hence  ((All (a,PA,G)) 'imp' u) . x = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((All (a,PA,G)) 'imp' u) . x = TRUE ; ::_thesis: verum
end;
hence  (All (a,PA,G)) 'imp' u = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_4:19
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' u
proof
let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' u
let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' u
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' u
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex (u,PA,G) '<' u )
assume  u is_independent_of PA,G ; ::_thesis: Ex (u,PA,G) '<' u
then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8;
 for z being Element of Y holds ((Ex (u,PA,G)) 'imp' u) . z = TRUE
proof
let z be Element of Y; ::_thesis: ((Ex (u,PA,G)) 'imp' u) . z = TRUE
A2: ((Ex (u,PA,G)) 'imp' u) . z = ('not' ((Ex (u,PA,G)) . z)) 'or' (u . z) by BVFUNC_1:def_8;
A3: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6;
now__::_thesis:_(_(_u_._z_=_TRUE_&_((Ex_(u,PA,G))_'imp'_u)_._z_=_TRUE_)_or_(_u_._z_=_FALSE_&_((Ex_(u,PA,G))_'imp'_u)_._z_=_TRUE_)_)
percases ( u . z = TRUE or u . z = FALSE ) by XBOOLEAN:def_3;
case u . z = TRUE ; ::_thesis: ((Ex (u,PA,G)) 'imp' u) . z = TRUE
hence  ((Ex (u,PA,G)) 'imp' u) . z = TRUE by A2; ::_thesis: verum
end;
case u . z = FALSE ; ::_thesis: ((Ex (u,PA,G)) 'imp' u) . z = TRUE
then  for x1 being Element of Y holds
( not x1 in EqClass (z,(CompF (PA,G))) or not u . x1 = TRUE ) by A1, A3, BVFUNC_1:def_15;
then  (B_SUP (u,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  ((Ex (u,PA,G)) 'imp' u) . z = TRUE by A2; ::_thesis: verum
end;
end;
end;
hence  ((Ex (u,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: verum
end;
then  (Ex (u,PA,G)) 'imp' u = I_el Y by BVFUNC_1:def_11;
hence  Ex (u,PA,G) '<' u by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_4:20
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
u '<' All (u,PA,G)
proof
let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
u '<' All (u,PA,G)
let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
u '<' All (u,PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
u '<' All (u,PA,G)
let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies u '<' All (u,PA,G) )
assume  u is_independent_of PA,G ; ::_thesis: u '<' All (u,PA,G)
then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8;
 for z being Element of Y holds (u 'imp' (All (u,PA,G))) . z = TRUE
proof
let z be Element of Y; ::_thesis: (u 'imp' (All (u,PA,G))) . z = TRUE
A2: (u 'imp' (All (u,PA,G))) . z = ('not' (u . z)) 'or' ((All (u,PA,G)) . z) by BVFUNC_1:def_8;
A3: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6;
now__::_thesis:_(_(_u_._z_=_FALSE_&_(u_'imp'_(All_(u,PA,G)))_._z_=_TRUE_)_or_(_u_._z_=_TRUE_&_(u_'imp'_(All_(u,PA,G)))_._z_=_TRUE_)_)
percases ( u . z = FALSE or u . z = TRUE ) by XBOOLEAN:def_3;
case u . z = FALSE ; ::_thesis: (u 'imp' (All (u,PA,G))) . z = TRUE
hence  (u 'imp' (All (u,PA,G))) . z = TRUE by A2; ::_thesis: verum
end;
case u . z = TRUE ; ::_thesis: (u 'imp' (All (u,PA,G))) . z = TRUE
then  for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE by A1, A3, BVFUNC_1:def_15;
then  (All (u,PA,G)) . z = TRUE by BVFUNC_1:def_16;
hence  (u 'imp' (All (u,PA,G))) . z = TRUE by A2; ::_thesis: verum
end;
end;
end;
hence  (u 'imp' (All (u,PA,G))) . z = TRUE ; ::_thesis: verum
end;
then  u 'imp' (All (u,PA,G)) = I_el Y by BVFUNC_1:def_11;
hence  u '<' All (u,PA,G) by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_4:21
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PB,G holds
All (u,PA,G) '<' All (u,PB,G)
proof
let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PB,G holds
All (u,PA,G) '<' All (u,PB,G)
let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PB,G holds
All (u,PA,G) '<' All (u,PB,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for PA, PB being a_partition of Y st u is_independent_of PB,G holds
All (u,PA,G) '<' All (u,PB,G)
let PA, PB be a_partition of Y; ::_thesis: ( u is_independent_of PB,G implies All (u,PA,G) '<' All (u,PB,G) )
assume  u is_independent_of PB,G ; ::_thesis: All (u,PA,G) '<' All (u,PB,G)
then A1: u is_dependent_of CompF (PB,G) by BVFUNC_2:def_8;
 for z being Element of Y holds ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE
proof
let z be Element of Y; ::_thesis: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE
A2: ( z in EqClass (z,(CompF (PB,G))) & EqClass (z,(CompF (PB,G))) in CompF (PB,G) ) by EQREL_1:def_6;
A3: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = ('not' ((All (u,PA,G)) . z)) 'or' ((All (u,PB,G)) . z) by BVFUNC_1:def_8;
A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
now__::_thesis:_(_(_(All_(u,PA,G))_._z_=_FALSE_&_((All_(u,PA,G))_'imp'_(All_(u,PB,G)))_._z_=_TRUE_)_or_(_(All_(u,PA,G))_._z_=_TRUE_&_((All_(u,PA,G))_'imp'_(All_(u,PB,G)))_._z_=_TRUE_)_)
percases ( (All (u,PA,G)) . z = FALSE or (All (u,PA,G)) . z = TRUE ) by XBOOLEAN:def_3;
case (All (u,PA,G)) . z = FALSE ; ::_thesis: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE
hence  ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE by A3; ::_thesis: verum
end;
case (All (u,PA,G)) . z = TRUE ; ::_thesis: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE
then  u . z = TRUE by A4, BVFUNC_1:def_16;
then  for x being Element of Y st x in EqClass (z,(CompF (PB,G))) holds
u . x = TRUE by A1, A2, BVFUNC_1:def_15;
then  (All (u,PB,G)) . z = TRUE by BVFUNC_1:def_16;
hence  ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE by A3; ::_thesis: verum
end;
end;
end;
hence  ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE ; ::_thesis: verum
end;
then  (All (u,PA,G)) 'imp' (All (u,PB,G)) = I_el Y by BVFUNC_1:def_11;
hence  All (u,PA,G) '<' All (u,PB,G) by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_4:22
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' Ex (u,PB,G)
proof
let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' Ex (u,PB,G)
let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' Ex (u,PB,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' Ex (u,PB,G)
let PA, PB be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex (u,PA,G) '<' Ex (u,PB,G) )
assume  u is_independent_of PA,G ; ::_thesis: Ex (u,PA,G) '<' Ex (u,PB,G)
then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8;
 for z being Element of Y holds ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE
proof
let z be Element of Y; ::_thesis: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE
A2: z in EqClass (z,(CompF (PB,G))) by EQREL_1:def_6;
A3: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = ('not' ((Ex (u,PA,G)) . z)) 'or' ((Ex (u,PB,G)) . z) by BVFUNC_1:def_8;
A4: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6;
now__::_thesis:_(_(_(Ex_(u,PB,G))_._z_=_TRUE_&_((Ex_(u,PA,G))_'imp'_(Ex_(u,PB,G)))_._z_=_TRUE_)_or_(_(Ex_(u,PB,G))_._z_=_FALSE_&_((Ex_(u,PA,G))_'imp'_(Ex_(u,PB,G)))_._z_=_TRUE_)_)
percases ( (Ex (u,PB,G)) . z = TRUE or (Ex (u,PB,G)) . z = FALSE ) by XBOOLEAN:def_3;
case (Ex (u,PB,G)) . z = TRUE ; ::_thesis: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE
hence  ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE by A3; ::_thesis: verum
end;
case (Ex (u,PB,G)) . z = FALSE ; ::_thesis: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE
then  u . z <> TRUE by A2, BVFUNC_1:def_17;
then  for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not u . x = TRUE ) by A1, A4, BVFUNC_1:def_15;
then  (B_SUP (u,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE by A3; ::_thesis: verum
end;
end;
end;
hence  ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE ; ::_thesis: verum
end;
then  (Ex (u,PA,G)) 'imp' (Ex (u,PB,G)) = I_el Y by BVFUNC_1:def_11;
hence  Ex (u,PA,G) '<' Ex (u,PB,G) by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_4:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'eqv' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE )
assume A1: (All ((a 'eqv' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
A2: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = 'not' (((All (a,PA,G)) . z) 'xor' ((All (b,PA,G)) . z)) by BVFUNC_1:def_9
.= ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z))) 'or' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z)) by XBOOLEAN:8
.= ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) 'or' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)))) by XBOOLEAN:8
.= ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) 'or' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) by XBOOLEAN:8
.= (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) 'or' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) by XBOOLEAN:138
.= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE) by XBOOLEAN:138
.= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) ;
percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ) ;
supposeA3: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
then  (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, A3, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA4: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A5: x1 in EqClass (z,(CompF (PA,G))) and
A6: b . x1 <> TRUE ;
A7: a . x1 = TRUE by A4, A5;
(a 'eqv' b) . x1 = 'not' ((a . x1) 'xor' (b . x1)) by BVFUNC_1:def_9
.= FALSE by A6, A7, XBOOLEAN:def_3 ;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A1, A5, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA8: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A9: x1 in EqClass (z,(CompF (PA,G))) and
A10: a . x1 <> TRUE ;
A11: b . x1 = TRUE by A8, A9;
(a 'eqv' b) . x1 = 'not' ((a . x1) 'xor' (b . x1)) by BVFUNC_1:def_9
.= FALSE by A10, A11, XBOOLEAN:def_3 ;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A1, A9, BVFUNC_1:def_16; ::_thesis: verum
end;
supposeA12: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
then  (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, A12, BVFUNC_1:def_16; ::_thesis: verum
end;
end;
end;

theorem :: BVFUNC_4:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let PA be a_partition of Y; ::_thesis: All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a '&' b),PA,G)) . z = TRUE or (a '&' (All (b,PA,G))) . z = TRUE )
assume A1: (All ((a '&' b),PA,G)) . z = TRUE ; ::_thesis: (a '&' (All (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 consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: a . x1 <> TRUE ;
 (a '&' b) . x1 = TRUE by A1, A3, BVFUNC_1:def_16;
then A5: (a . x1) '&' (b . x1) = TRUE by MARGREL1:def_20;
 a . x1 = FALSE by A4, XBOOLEAN:def_3;
hence  contradiction by A5; ::_thesis: verum
end;
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 consider x1 being Element of Y such that
A6: x1 in EqClass (z,(CompF (PA,G))) and
A7: b . x1 <> TRUE ;
 (a '&' b) . x1 = TRUE by A1, A6, BVFUNC_1:def_16;
then A8: (a . x1) '&' (b . x1) = TRUE by MARGREL1:def_20;
 b . x1 = FALSE by A7, XBOOLEAN:def_3;
hence  contradiction by A8; ::_thesis: verum
end;
then A9: (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16;
 z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
then  a . z = TRUE by A2;
then (a '&' (All (b,PA,G))) . z = TRUE '&' TRUE by A9, MARGREL1:def_20
.= TRUE ;
hence  (a '&' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_4:25
for Y being non empty set
for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
proof
let Y be non empty set ; ::_thesis: for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let a, u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) 'imp' u) . z = TRUE or (Ex ((a 'imp' u),PA,G)) . z = TRUE )
A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6;
assume  ((All (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE
then A2: ('not' ((All (a,PA,G)) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def_8;
A3: ( 'not' ((All (a,PA,G)) . z) = TRUE or 'not' ((All (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_'not'_((All_(a,PA,G))_._z)_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_or_(_u_._z_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_)
percases ( 'not' ((All (a,PA,G)) . z) = TRUE or u . z = TRUE ) by A2, A3;
case 'not' ((All (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' u),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 by BVFUNC_1:def_16;
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  (a 'imp' u) . x1 <> TRUE by A4;
then  (a 'imp' u) . x1 = FALSE by XBOOLEAN:def_3;
then A6: ('not' (a . x1)) 'or' (u . x1) = FALSE by BVFUNC_1:def_8;
 ( 'not' (a . x1) = TRUE or 'not' (a . x1) = FALSE ) by XBOOLEAN:def_3;
hence  contradiction by A5, A6; ::_thesis: verum
end;
hence  (Ex ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_17; ::_thesis: verum
end;
caseA7: u . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . 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  (a 'imp' u) . z <> TRUE by A1;
then  (a 'imp' u) . z = FALSE by XBOOLEAN:def_3;
then  ('not' (a . z)) 'or' (u . z) = FALSE by BVFUNC_1:def_8;
hence  contradiction by A7; ::_thesis: verum
end;
hence  (Ex ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_4:26
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 st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
let PA be a_partition of Y; ::_thesis: ( a 'eqv' b = I_el Y implies (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y )
assume A1: a 'eqv' b = I_el Y ; ::_thesis: (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
then  b 'imp' a = I_el Y by Th10;
then A2: ('not' b) 'or' a = I_el Y by Th8;
 a 'imp' b = I_el Y by A1, Th10;
then A3: ('not' a) 'or' b = I_el Y by Th8;
 for z being Element of Y holds ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
proof
let z be Element of Y; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
A4: now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_)
assume that
A5: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE and
A6: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
consider x1 being Element of Y such that
A7: x1 in EqClass (z,(CompF (PA,G))) and
A8: b . x1 <> TRUE by A6;
A9: a . x1 = TRUE by A5, A7;
A10: b . x1 = FALSE by A8, XBOOLEAN:def_3;
(('not' a) 'or' b) . x1 = (('not' a) . x1) 'or' (b . x1) by BVFUNC_1:def_4
.= FALSE 'or' FALSE by A10, A9, MARGREL1:def_19
.= FALSE ;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A3, BVFUNC_1:def_11; ::_thesis: verum
end;
A11: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_)
assume that
A12: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) and
A13: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
consider x1 being Element of Y such that
A14: x1 in EqClass (z,(CompF (PA,G))) and
A15: a . x1 <> TRUE by A12;
A16: b . x1 = TRUE by A13, A14;
A17: a . x1 = FALSE by A15, XBOOLEAN:def_3;
(('not' b) 'or' a) . x1 = (('not' b) . x1) 'or' (a . x1) by BVFUNC_1:def_4
.= FALSE 'or' FALSE by A17, A16, MARGREL1:def_19
.= FALSE ;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, BVFUNC_1:def_11; ::_thesis: verum
end;
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = ((All (a,PA,G)) 'imp' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) by Th7
.= (('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) by Th8
.= (('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (('not' (All (b,PA,G))) 'or' (All (a,PA,G))) by Th8
.= ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G))) by BVFUNC_1:12
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G))))) 'or' ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G))) by BVFUNC_1:12
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G))))) 'or' ((('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by BVFUNC_1:12
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y)) 'or' ((('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by Th5
.= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y)) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by Th5
.= (('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by BVFUNC_1:9
.= (('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G))) by BVFUNC_1:9 ;
then A18: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) by BVFUNC_1:def_4
.= ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) by MARGREL1:def_20
.= ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def_20
.= (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def_19
.= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def_19 ;
A19: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_)
assume that
A20: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) and
A21: ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
 (B_INF (b,(CompF (PA,G)))) . z = FALSE by A21, BVFUNC_1:def_16;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A18, A20, BVFUNC_1:def_16; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_)
assume that
A22: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE and
A23: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
b . x = TRUE ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE
 (B_INF (b,(CompF (PA,G)))) . z = TRUE by A23, BVFUNC_1:def_16;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A18, A22, BVFUNC_1:def_16; ::_thesis: verum
end;
hence  ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A4, A11, A19; ::_thesis: verum
end;
hence  (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_4:27
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 st a 'eqv' b = I_el Y holds
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
let PA be a_partition of Y; ::_thesis: ( a 'eqv' b = I_el Y implies (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y )
assume A1: a 'eqv' b = I_el Y ; ::_thesis: (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
then  b 'imp' a = I_el Y by Th10;
then A2: ('not' b) 'or' a = I_el Y by Th8;
 a 'imp' b = I_el Y by A1, Th10;
then A3: ('not' a) 'or' b = I_el Y by Th8;
 for z being Element of Y holds ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE
proof
let z be Element of Y; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) '&' ((Ex (b,PA,G)) 'imp' (Ex (a,PA,G))) by Th7
.= (('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' ((Ex (b,PA,G)) 'imp' (Ex (a,PA,G))) by Th8
.= (('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (('not' (Ex (b,PA,G))) 'or' (Ex (a,PA,G))) by Th8
.= ((('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (Ex (a,PA,G))) by BVFUNC_1:12
.= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' ('not' (Ex (b,PA,G))))) 'or' ((('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (Ex (a,PA,G))) by BVFUNC_1:12
.= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' ('not' (Ex (b,PA,G))))) 'or' ((('not' (Ex (a,PA,G))) '&' (Ex (a,PA,G))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by BVFUNC_1:12
.= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' (O_el Y)) 'or' ((('not' (Ex (a,PA,G))) '&' (Ex (a,PA,G))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by Th5
.= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' (O_el Y)) 'or' ((O_el Y) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by Th5
.= (('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((O_el Y) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by BVFUNC_1:9
.= (('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G))) by BVFUNC_1:9 ;
then A4: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z) 'or' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) by BVFUNC_1:def_4
.= ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) by MARGREL1:def_20
.= ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) by MARGREL1:def_20
.= (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) by MARGREL1:def_19
.= (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z))) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) by MARGREL1:def_19 ;
percases ( ( 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))) & 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 ) ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & 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 ) ) ) ) ;
supposeA5: ( 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))) & b . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17;
hence  ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A4, A5, BVFUNC_1:def_17; ::_thesis: verum
end;
supposeA6: ( 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)) 'eqv' (Ex (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A7: x1 in EqClass (z,(CompF (PA,G))) and
A8: a . x1 = TRUE ;
 b . x1 <> TRUE by A6, A7;
then A9: b . x1 = FALSE by XBOOLEAN:def_3;
(('not' a) 'or' b) . x1 = (('not' a) . x1) 'or' (b . x1) by BVFUNC_1:def_4
.= FALSE 'or' FALSE by A8, A9, MARGREL1:def_19
.= FALSE ;
hence  ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A3, BVFUNC_1:def_11; ::_thesis: verum
end;
supposeA10: ( ( 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))) & b . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A11: x1 in EqClass (z,(CompF (PA,G))) and
A12: b . x1 = TRUE ;
 a . x1 <> TRUE by A10, A11;
then A13: a . x1 = FALSE by XBOOLEAN:def_3;
(('not' b) 'or' a) . x1 = (('not' b) . x1) 'or' (a . x1) by BVFUNC_1:def_4
.= FALSE 'or' FALSE by A12, A13, MARGREL1:def_19
.= FALSE ;
hence  ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A2, BVFUNC_1:def_11; ::_thesis: verum
end;
supposeA14: ( ( 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)) 'eqv' (Ex (b,PA,G))) . z = TRUE
then  (B_SUP (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17;
hence  ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A4, A14, BVFUNC_1:def_17; ::_thesis: verum
end;
end;
end;
hence  (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;